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

Axiom	ax-zunle-pritu 601	Leftward and rightward are opposite.
⊢ go ko'a zunle ko'e ko'i gi ko'e pritu ko'a ko'i

Axiom	ax-gapru-cnita 602	Upward and downward are opposite.
⊢ go ko'a gapru ko'e ko'i gi ko'e cnita ko'a ko'i

5.3 Minkowski spacetime

5.3.1 {cabna}

Syntax	sbcabna 603
selbri cabna

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

5.3.2 {xlane}

Syntax	sbxlane 605
selbri xlane

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

5.3.3 {balvi}, {purci}

Syntax	sbbalvi 607
selbri balvi

Syntax	sbpurci 608
selbri purci

Axiom	ax-balvi-purci 609	{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 610
selbri ki'irni'i

Definition	df-kihirnihi 611*	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 612	{ki'irni'i} is reflexive. (Contributed by la korvo, 13-Aug-2024.)
⊢ ko'a ki'irni'i ko'a

Theorem	kihirnihi-kinra 613	{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 614	{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 615
selbri ki'irkanxe

Definition	df-kihirkanxe 616*	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 617
selbri ki'irvlina

Definition	df-kihirvlina 618*	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 619
selbri lujna'u

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

Axiom	ax-comp-pa 621	One is a complex number. One of Megill's axioms.
⊢ li 1 +i 0 lujna'u

Axiom	ax-comp-kaho 622	The imaginary unit is a complex number. One of Megill's axioms.
⊢ li 0 +i 1 lujna'u

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

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

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

Axiom	ax-comp-1ne0 626	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 627
selbri mrena'u

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

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

6.3 Functions I

6.3.1 {fancu}

Syntax	sbfancu 630
selbri fancu

Definition	df-fancu 631*	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 632*	Inference form of df-fancu 631 (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 633*	Inference form of df-fancu 631 (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 634
selbri pagyfancu

Definition	df-pagyfancu 635*	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 636
selbri mapti

Definition	df-mapti 637	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 638	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 639
selbri drata

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

6.4.3 {frica}

Syntax	sbfrica 641
selbri frica

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

6.4.4 {nenri}

Syntax	sbnenri 643
selbri nenri

Axiom	ax-nenri-trans 644	{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 645
selbri fatne

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

6.4.6 {rinka}

Syntax	sbrinka 647
selbri rinka

Axiom	ax-rinka-balvi 648	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 649
selbri skari

Axiom	ax-skari-ckaji 650	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 651	All {skaselbri} are {selbri}.
skaselbri bu'a selbri bu'a

Definition	df-skaselbri 652*	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 653*	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 654
selbri lanzu

Syntax	sblazmihu 655
selbri lazmi'u

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

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

6.6 Generated baseline ontology

Syntax	sbbakni 658	### Generated baseline ontology ###
selbri bakni

Syntax	sbbambu 659
selbri bambu

Syntax	sbbanfi 660
selbri banfi

Syntax	sbbifce 661
selbri bifce

Syntax	sbcindu 662
selbri cindu

Syntax	sbcinfo 663
selbri cinfo

Syntax	sbcinki 664
selbri cinki

Syntax	sbcipni 665
selbri cipni

Syntax	sbcivla 666
selbri civla

Syntax	sbckunu 667
selbri ckunu

Syntax	sbcribe 668
selbri cribe

Syntax	sbcurnu 669
selbri curnu

Syntax	sbdanlu 670
selbri danlu

Syntax	sbdatka 671
selbri datka

Syntax	sbfinpe 672
selbri finpe

Syntax	sbgerku 673
selbri gerku

Syntax	sbgunse 674
selbri gunse

Syntax	sbjalra 675
selbri jalra

Syntax	sbjipci 676
selbri jipci

Syntax	sbjukni 677
selbri jukni

Syntax	sbkanba 678
selbri kanba

Syntax	sbkumte 679
selbri kumte

Syntax	sblabno 680
selbri labno

Syntax	sblanme 681
selbri lanme

Syntax	sblelxe 682
selbri lelxe

Syntax	sblorxu 683
selbri lorxu

Syntax	sbmabru 684
selbri mabru

Syntax	sbmanti 685
selbri manti

Syntax	sbmarna 686
selbri marna

Syntax	sbmirli 687
selbri mirli

Syntax	sbmlatu 688
selbri mlatu

Syntax	sbnimre 689
selbri nimre

Syntax	sbpoplu 690
selbri poplu

Syntax	sbractu 691
selbri ractu

Syntax	sbratcu 692
selbri ratcu

Syntax	sbremna 693
selbri remna

Syntax	sbrespa 694
selbri respa

Syntax	sbrozgu 695
selbri rozgu

Syntax	sbsfani 696
selbri sfani

Syntax	sbsince 697
selbri since

Syntax	sbsluni 698
selbri sluni

Syntax	sbsmacu 699
selbri smacu

Syntax	sbsmani 700
selbri smani

< 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-977

< Previous Next >