P. 7 of Theorem List - brismu bridi

Home	brismu bridi Theorem List (p. 7 of 9)	< 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.2 {xlane}

Syntax	sbxlane 601
selbri xlane

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

5.3.3 {balvi}, {purci}

Syntax	sbbalvi 603
selbri balvi

Syntax	sbpurci 604
selbri purci

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

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

Theorem	kihirnihi-kinra 609	{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 610	{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 611
selbri ki'irkanxe

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

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

Syntax	pc 616*	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 617	One is a complex number. One of Megill's axioms.
⊢ li 1 ka'o0 lujna'u

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

Axiom	ax-comp-suhi 619*	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 620*	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 621	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 622	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 623
selbri mrena'u

Axiom	ax-real-suhi 624*	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 625*	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 626
selbri fancu

Definition	df-fancu 627*	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 628*	Inference form of df-fancu 627 (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 629*	Inference form of df-fancu 627 (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 630
selbri pagyfancu

Definition	df-pagyfancu 631*	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 632
selbri mapti

Definition	df-mapti 633	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 634	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 635
selbri drata

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

6.4.3 {frica}

Syntax	sbfrica 637
selbri frica

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

6.4.4 {nenri}

Syntax	sbnenri 639
selbri nenri

Axiom	ax-nenri-trans 640	{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 641
selbri fatne

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

6.4.6 {rinka}

Syntax	sbrinka 643
selbri rinka

Axiom	ax-rinka-balvi 644	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 645
selbri skari

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

Definition	df-skaselbri 648*	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 649*	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 650
selbri lanzu

Syntax	sblazmihu 651
selbri lazmi'u

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

Definition	df-lazmihu 653	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 654
selbri bakni

Syntax	sbbambu 655
selbri bambu

Syntax	sbbanfi 656
selbri banfi

Syntax	sbbifce 657
selbri bifce

Syntax	sbcindu 658
selbri cindu

Syntax	sbcinfo 659
selbri cinfo

Syntax	sbcinki 660
selbri cinki

Syntax	sbcipni 661
selbri cipni

Syntax	sbcivla 662
selbri civla

Syntax	sbckunu 663
selbri ckunu

Syntax	sbcribe 664
selbri cribe

Syntax	sbcurnu 665
selbri curnu

Syntax	sbdanlu 666
selbri danlu

Syntax	sbdatka 667
selbri datka

Syntax	sbfinpe 668
selbri finpe

Syntax	sbgerku 669
selbri gerku

Syntax	sbgunse 670
selbri gunse

Syntax	sbjalra 671
selbri jalra

Syntax	sbjipci 672
selbri jipci

Syntax	sbjukni 673
selbri jukni

Syntax	sbkanba 674
selbri kanba

Syntax	sbkumte 675
selbri kumte

Syntax	sblabno 676
selbri labno

Syntax	sblanme 677
selbri lanme

Syntax	sblelxe 678
selbri lelxe

Syntax	sblorxu 679
selbri lorxu

Syntax	sbmabru 680
selbri mabru

Syntax	sbmanti 681
selbri manti

Syntax	sbmarna 682
selbri marna

Syntax	sbmirli 683
selbri mirli

Syntax	sbmlatu 684
selbri mlatu

Syntax	sbnimre 685
selbri nimre

Syntax	sbpoplu 686
selbri poplu

Syntax	sbractu 687
selbri ractu

Syntax	sbratcu 688
selbri ratcu

Syntax	sbremna 689
selbri remna

Syntax	sbrespa 690
selbri respa

Syntax	sbrozgu 691
selbri rozgu

Syntax	sbsfani 692
selbri sfani

Syntax	sbsince 693
selbri since

Syntax	sbsluni 694
selbri sluni

Syntax	sbsmacu 695
selbri smacu

Syntax	sbsmani 696
selbri smani

Syntax	sbspati 697
selbri spati

Syntax	sbsrasu 698
selbri srasu

Syntax	sbtirxu 699
selbri tirxu

Syntax	sbtoldi 700
selbri toldi

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

< Previous Next >