P. 7 of Theorem List - brismu bridi

Home	brismu bridi Theorem List (p. 7 of 10)	< Previous Next >
		Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List

**Theorem List for brismu bridi -** 601-700 *Has distinct variable group(s)
Type	Label	Description
Statement

5.3 Minkowski spacetime

5.3.1 {cabna}

Syntax	sbcabna 601
selbri cabna

Axiom	ax-cabna-sym 602	{cabna} is symmetric.
⊢ go ko'a cabna ko'e gi ko'e cabna ko'a

5.3.2 {xlane}

Syntax	sbxlane 603
selbri xlane

Axiom	ax-xlane-sym 604	{xlane} is symmetric.
⊢ go ko'a xlane ko'e gi ko'e xlane ko'a

5.3.3 {balvi}, {purci}

Syntax	sbbalvi 605
selbri balvi

Syntax	sbpurci 606
selbri purci

Axiom	ax-balvi-purci 607	{balvi} and {purci} are each other's daggers.
⊢ go ko'a balvi ko'e gi ko'e purci ko'a

PART 6 RELATIONAL LOGIC

6.1 Lattice of relations

6.1.1 {ki'irni'i}

Syntax	sbkihirnihi 608
selbri ki'irni'i

Definition	df-kihirnihi 609*	Definition of {ki'irni'i} in terms of {ckini} and {na.a}. Unlike prior definitions, this one does not require any terbri inspection.
⊢ go ko'a ki'irni'i ko'e gi ro da zo'u ro de zo'u da ckini de ko'a na.a ko'e

Theorem	kihirnihi-refl 610	{ki'irni'i} is reflexive. (Contributed by la korvo, 13-Aug-2024.)
⊢ ko'a ki'irni'i ko'a

Theorem	kihirnihi-kinra 611	{ki'irni'i} is reflexive over any domain. (Contributed by la korvo, 13-Aug-2024.)
⊢ 1 ka ce'u ki'irni'i ce'u kei kinra ko'e

Axiom	ax-kihirnihi-trans 612	{ki'irni'i} is transitive.
⊢ ganai ge ko'a ki'irni'i ko'e gi ko'e ki'irni'i ko'i gi ko'a ki'irni'i ko'i

6.1.2 {ki'irkanxe}

Syntax	sbkihirkanxe 613
selbri ki'irkanxe

Definition	df-kihirkanxe 614*	Definition of {ki'irkanxe}
⊢ 1 ka ce'u bu'a je bu'e ce'u kei ki'irkanxe 1 ka ce'u bu'a ce'u kei 1 ka ce'u bu'e ce'u kei

6.1.3 {ki'irvlina}

Syntax	sbkihirvlina 615
selbri ki'irvlina

Definition	df-kihirvlina 616*	Definition of {ki'irvlina}
⊢ 1 ka ce'u bu'a ja bu'e ce'u kei ki'irvlina 1 ka ce'u bu'a ce'u kei 1 ka ce'u bu'e ce'u kei

6.2 Complex numbers

6.2.1 Complex number predicate: {lujna'u}

Syntax	sblujnahu 617
selbri lujna'u

Syntax	pc 618*	Syntax for complex numbers. (Contributed by la korvo, 3-Jan-2025.)
PA ku'i'a PA ku'i'e PA ku'i'a ka'oku'i'e

Axiom	ax-comp-pa 619	One is a complex number. One of Megill's axioms.
⊢ li 1 ka'o0 lujna'u

Axiom	ax-comp-kaho 620	The imaginary unit is a complex number. One of Megill's axioms.
⊢ li 0 ka'o1 lujna'u

Axiom	ax-comp-suhi 621*	Complex numbers are closed under addition. One of Megill's axioms.
⊢ ganai li ku'i'a .e li ku'i'e lujna'ugi li + ku'i'a ku'i'e lujna'u

Axiom	ax-comp-pihi 622*	Complex numbers are closed under multiplication. One of Megill's axioms.
⊢ ganai li ku'i'a .e li ku'i'e lujna'ugi li * ku'i'a ku'i'e lujna'u

Axiom	ax-comp-i2m1 623	The imaginary unit is a square root of negative one. One of Megill's axioms.
⊢ li + * 0 ka'o1 0 ka'o1 1 du li 0

Axiom	ax-comp-1ne0 624	One is not zero. One of Megill's axioms.
⊢ naku li 1 du li 0

6.2.2 Real number predicate: {mrena'u}

Syntax	sbmrenahu 625
selbri mrena'u

Axiom	ax-real-suhi 626*	Real numbers are closed under addition. One of Megill's axioms.
⊢ ganai li ku'i'a .e li ku'i'e mrena'ugi li + ku'i'a ku'i'e mrena'u

Axiom	ax-real-pihi 627*	Real numbers are closed under multiplication. One of Megill's axioms.
⊢ ganai li ku'i'a .e li ku'i'e mrena'ugi li * ku'i'a ku'i'e mrena'u

6.3 Functions I

6.3.1 {fancu}

Syntax	sbfancu 628
selbri fancu

Definition	df-fancu 629*	Definition of {fancu}. Note that the name of the function is neither unique nor concrete.
⊢ go ko'a fancu ko'e ko'i ko'o gi ro da poi ke'a cmima ko'e ku'o zo'u 1 de zo'u ge de cmima ko'i gi da ckini de ko'o

Theorem	fancui 630*	Inference form of df-fancu 629 (Contributed by la korvo, 12-Aug-2024.)
⊢ ko'a fancu ko'e ko'i ko'o ⊢ ro da poi ke'a cmima ko'e ku'o zo'u 1 de zo'u ge de cmima ko'i gi da ckini de ko'o

Theorem	fancuii 631*	Inference form of df-fancu 629 (Contributed by la korvo, 12-Aug-2024.)
⊢ ko'a fancu ko'e ko'i ko'o ⊢ de cmima ko'e ⊢ 1 da zo'u ge da cmima ko'i gi de ckini da ko'o

6.3.2 {pagyfancu}

Syntax	sbpagyfancu 632
selbri pagyfancu

Definition	df-pagyfancu 633*	Definition of {pagyfancu} in terms of {ki'irni'i}.
go su'o da zo'u su'o de zo'u su'o di zo'u da pagyfancu de di 1 ka ce'u bu'a ce'u kei gi 1 ka su'o da zo'u ce'u .e ce'u bu'a da kei ki'irni'i 1 ka ce'u du ce'u kei

6.4 Assorted claims

6.4.1 {mapti}

Syntax	sbmapti 634
selbri mapti

Definition	df-mapti 635	Proposed definition of {mapti} as a witness to an inhabited bijection.
⊢ go ko'a mapti ko'e ko'i gi ge ko'a ckini ko'e ko'i gi ge ro da zo'u ganai da ckini ko'e ko'i gi da du ko'a gi ro da zo'u ganai ko'a ckini da ko'i gi da du ko'e

Theorem	mapti-ckini 636	Under postulated definitions of la xorxes and la korvo, {mapti} is a subrelation of {ckini}. (Contributed by la korvo, 22-Aug-2024.)
⊢ ganai ko'a mapti ko'e ko'i gi ko'a ckini ko'e ko'i

6.4.2 {drata}

Syntax	sbdrata 637
selbri drata

Axiom	ax-drata-irrefl 638	{drata} is irreflexive.
⊢ naku ko'a drata ko'a ko'e

6.4.3 {frica}

Syntax	sbfrica 639
selbri frica

Axiom	ax-frica-irrefl 640	{frica} is irreflexive.
⊢ naku ko'a frica ko'a ko'e

6.4.4 {nenri}

Syntax	sbnenri 641
selbri nenri

Axiom	ax-nenri-trans 642	{nenri} is transitive.
⊢ ganai ge ko'a nenri ko'e gi ko'e nenri ko'i gi ko'a nenri ko'i

6.4.5 {fatne}

Syntax	sbfatne 643
selbri fatne

Axiom	ax-fatne-sym 644	{fatne} is symmetric.
⊢ go ko'a fatne ko'e gi ko'e fatne ko'a

6.4.6 {rinka}

Syntax	sbrinka 645
selbri rinka

Axiom	ax-rinka-balvi 646	Physical causation implies spatiotemporal causation.
⊢ ganai ko'a rinka ko'e ko'i gi ko'a balvi ko'e

6.5 Ontological classes

6.5.1 Colors: {skari} The schema for colors classifies one type, the colors ({skaselbri}).

Syntax	sbskari 647
selbri skari

Axiom	ax-skari-ckaji 648	Colors are extensionally defined in terms of {skari}.
⊢ ganai ko'a skari ko'e ko'i ko'o gi ko'a ckaji ko'e

Syntax	sbska 649	All {skaselbri} are {selbri}.
skaselbri bu'a selbri bu'a

Definition	df-skaselbri 650*	To be colored is to appear colored in a certain context.
skaselbri bu'a ⊢ go ko'a bu'a gi su'o da zo'u su'o de zo'u ko'a skari 1 ka ce'u bu'a kei da de

Axiom	ax-xinmo2-skari2 651*	Definitionally, xinmo2 is drawn from skari2.
⊢ ganai ko'a se xinmo ko'e gi su'o da zo'u su'o de zo'u su'o di zo'u ko'a se skari da de di

6.5.2 Families: {lanzu}

Syntax	sblanzu 652
selbri lanzu

Syntax	sblazmihu 653
selbri lazmi'u

Axiom	ax-lanzu-cmima 654	{lanzu} is a subrelation of {cmima} as implied by df-lazmihu 655 and baseline notes.
⊢ ganai ko'a lanzuko'e ko'i gi ko'e cmima ko'a

Definition	df-lazmihu 655	Definition of {lazmi'u} in terms of {lanzu} and {cmima} from the baseline notes.
⊢ go ko'a lazmi'uko'e gi su'o da poi ke'a lanzuku'o zo'u ko'a mintu ko'e 1 ka ce'u cmima da kei

6.6 Generated baseline ontology

Syntax	sbbakni 656
selbri bakni

Syntax	sbbambu 657
selbri bambu

Syntax	sbbanfi 658
selbri banfi

Syntax	sbbifce 659
selbri bifce

Syntax	sbcindu 660
selbri cindu

Syntax	sbcinfo 661
selbri cinfo

Syntax	sbcinki 662
selbri cinki

Syntax	sbcipni 663
selbri cipni

Syntax	sbcivla 664
selbri civla

Syntax	sbckunu 665
selbri ckunu

Syntax	sbcribe 666
selbri cribe

Syntax	sbcurnu 667
selbri curnu

Syntax	sbdanlu 668
selbri danlu

Syntax	sbdatka 669
selbri datka

Syntax	sbfinpe 670
selbri finpe

Syntax	sbgerku 671
selbri gerku

Syntax	sbgunse 672
selbri gunse

Syntax	sbjalra 673
selbri jalra

Syntax	sbjipci 674
selbri jipci

Syntax	sbjukni 675
selbri jukni

Syntax	sbkanba 676
selbri kanba

Syntax	sbkumte 677
selbri kumte

Syntax	sblabno 678
selbri labno

Syntax	sblanme 679
selbri lanme

Syntax	sblelxe 680
selbri lelxe

Syntax	sblorxu 681
selbri lorxu

Syntax	sbmabru 682
selbri mabru

Syntax	sbmanti 683
selbri manti

Syntax	sbmarna 684
selbri marna

Syntax	sbmirli 685
selbri mirli

Syntax	sbmlatu 686
selbri mlatu

Syntax	sbnimre 687
selbri nimre

Syntax	sbpoplu 688
selbri poplu

Syntax	sbractu 689
selbri ractu

Syntax	sbratcu 690
selbri ratcu

Syntax	sbremna 691
selbri remna

Syntax	sbrespa 692
selbri respa

Syntax	sbrozgu 693
selbri rozgu

Syntax	sbsfani 694
selbri sfani

Syntax	sbsince 695
selbri since

Syntax	sbsluni 696
selbri sluni

Syntax	sbsmacu 697
selbri smacu

Syntax	sbsmani 698
selbri smani

Syntax	sbspati 699
selbri spati

Syntax	sbsrasu 700
selbri srasu

< Previous Next >

Page List Jump to page: Contents 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-975

< Previous Next >