P. 6 of Theorem List - brismu bridi

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

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

Theorem	sumji-no 501	Every natural number is equal to zero plus itself. (Contributed by la korvo, 30-Aug-2024.)
⊢ li ku'i'a sumji li 0 li ku'i'a

Axiom	ax-sumji-succ 502	Addition on natural numbers is well-founded and proceeds by successors. This is Robinson axiom 5.
⊢ su'o da zo'u ge ko'i sumji ko'a da gi ko'e kacli'e da ⊢ su'o da zo'u ge da sumji ko'a ko'e gi da kacli'e ko'i

3.1.7 Multiplication I: {pi'i}

Syntax	mpihi 503*
PA * ku'i'a ku'i'e

Axiom	ax-mul-zero 504	Multiplication with zero. A standard axiom of second-order arithmetic. Robinson's sixth axiom.
⊢ li * ku'i'a 0 du li 0

Axiom	ax-mul-succ 505*	Multiplication with successor. A standard axiom of second-order arithmetic.
⊢ li * ku'i'a 1+ ku'i'e du li + * ku'i'a ku'i'e ku'i'a

3.1.8 Multiplication II: {pilji}

Syntax	bpilji 506
selbri pilji

Definition	df-pilji 507*	Definition of {pilji} in terms of {*}.
⊢ go li ku'i'a pilji li ku'i'e ko'a gi li * ku'i'a ku'i'e du ko'a

Theorem	pilji-no 508	Every natural number times zero is zero. (Contributed by la korvo, 30-Aug-2024.)
⊢ li ku'i'a pilji li 0 li 0

Axiom	ax-pilji-succ 509	Multiplication on natural numbers is well-founded. This is Robinson axiom 7.
⊢ su'o da zo'u ge ko'i pilji ko'a da gi ko'e kacli'e da ⊢ su'o da zo'u ge ko'i sumji da ko'a gi da pilji ko'a ko'e

3.1.9 Comparison I: {kacme'a}

Syntax	bkacmeha 510
selbri kacme'a

Axiom	ax-gt-zero 511	Zero is not greater than any natural number. This is Robinson axiom 8.
⊢ naku zo'u ko'a kacme'a li 0

Theorem	gt-zero-ref 512	Refutation of any natural number less than zero. (Contributed by la korvo, 21-Jun-2024.)
⊢ ko'a kacme'a li 0 ⊢ gai'o

Definition	df-kacmeha 513	Recursive definition of {kacme'a}. This is Robinson axiom 11.
⊢ go ko'a kacme'a ko'e gi su'o da poi ke'a kacli'e ko'a zo'u ga da kacme'a ko'e gi da du ko'e

3.2 Exponents I: {tenfa}

Syntax	sbtenfa 514
selbri tenfa

3.3 Logarithms: {dugri}

Syntax	sbdugri 515
selbri dugri

Definition	df-dugri 516	{dugri} is a permutation of {tenfa}.
⊢ go ko'a dugri ko'e ko'i gi ko'a te se tenfa ko'e ko'i

Theorem	dugrii 517	Inference form of df-dugri 516 (Contributed by la korvo, 9-Aug-2023.)
⊢ ko'a dugri ko'e ko'i ⊢ ko'a te se tenfa ko'e ko'i

Theorem	dugriri 518	Inference form of df-dugri 516 (Contributed by la korvo, 9-Aug-2023.)
⊢ ko'a te se tenfa ko'e ko'i ⊢ ko'a dugri ko'e ko'i

3.4 Cardinality

3.4.1 {ka'au}

Syntax	mkahau 519	Syntax for cardinality over arbitrary sumti.
PA # ko'a

3.4.2 {kazmi}

Syntax	sbkazmi 520
selbri kazmi

Definition	df-kazmi 521	Definition of {kazmi} in terms of {#}.
⊢ go ko'a kazmi ko'e gi ko'a du li # ko'e

Axiom	ax-card-fun 522	Cardinality is a function on sets. An axiom of Fregean cardinality.
⊢ ganai ko'a .e ko'e kazmi ko'i gi ko'a du ko'e

Theorem	kazmi-funii 523	Inference form of ax-card-fun 522 (Contributed by la korvo, 31-Jul-2024.)
⊢ ko'a kazmi ko'i ⊢ ko'e kazmi ko'i ⊢ ko'a du ko'e

Axiom	ax-card-ex 524	A unary relation describes the empty set when it never holds. An axiom of Fregean cardinality.
⊢ go li 0 kazmi 1 ka ce'u bo'a kei gi naku zo'u su'o da zo'u da bo'a

PART 4 MEREOLOGY Mereology is an alternative to set theory. Where set theory focuses on elementhood, using {cmima}, mereology focuses on parthood, using {pagbu}.

4.1 Parthood

4.1.1 {pagbu}

Syntax	sbpagbu 525
selbri pagbu

Axiom	ax-pagbu-refl 526	Parthood is reflexive.
⊢ ko'a pagbu ko'a

Theorem	pagbu-kinra 527	{pagbu} is reflexive over any domain. (Contributed by la korvo, 31-Aug-2024.)
⊢ 1 ka ce'u pagbu ce'u kei kinra ko'e

Axiom	ax-pagbu-antisym 528	Parthood is antisymmetric.
⊢ ganai ge ko'a pagbu ko'e gi ko'e pagbu ko'a gi ko'a du ko'e

Theorem	pagbu-antisym 529	Inference form of ax-pagbu-antisym 528 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a pagbu ko'e ⊢ ko'e pagbu ko'a ⊢ ko'a du ko'e

Axiom	ax-pagbu-trans 530	Parthood is transitive.
⊢ ganai ge ko'a pagbu ko'e gi ko'e pagbu ko'i gi ko'a pagbu ko'i

Theorem	pagbu-trans 531	Inference form of ax-pagbu-trans 530 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a pagbu ko'e ⊢ ko'e pagbu ko'i ⊢ ko'a pagbu ko'i

Axiom	ax-pagbu-top 532	The universe exists.
⊢ su'o da zo'u ko'a pagbu da

Axiom	ax-pagbu-bot 533	The empty part exists.
⊢ su'o da zo'u da pagbu ko'a

4.1.2 {jompau}

Syntax	sbjompau 534
selbri jompau

Definition	df-jompau 535	Definition of {jompau} in terms of {pagbu}.
⊢ go ko'a jompau ko'e gi su'o da zo'u da pagbu ko'a .e ko'e

Theorem	jompaui 536	Inference form of df-jompau 535 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a jompau ko'e ⊢ su'o da zo'u da pagbu ko'a .e ko'e

Theorem	jompauri 537	Reverse inference form of df-jompau 535 (Contributed by la korvo, 4-Sep-2023.)
⊢ su'o da zo'u da pagbu ko'a .e ko'e ⊢ ko'a jompau ko'e

4.1.3 {kuzypau}

Syntax	sbkuzypau 538
selbri kuzypau

Definition	df-kuzypau 539	Definition of {kuzypau} in terms of {pagbu}.
⊢ go ko'a kuzypau ko'e gi su'o da zo'u ko'a .e ko'e pagbu da

Theorem	kuzypaui 540	Inference form of df-kuzypau 539 (Contributed by la korvo, 4-Sep-2023.)
⊢ ko'a kuzypau ko'e ⊢ su'o da zo'u ko'a .e ko'e pagbu da

Theorem	kuzypauri 541	Reverse inference form of df-kuzypau 539 (Contributed by la korvo, 4-Sep-2023.)
⊢ su'o da zo'u ko'a .e ko'e pagbu da ⊢ ko'a kuzypau ko'e

PART 5 SPACE & SPACETIME

5.1 Two-dimensional Euclidean space

5.1.1 Compass directions

Syntax	sbberti 542
selbri berti

Syntax	sbsnanu 543
selbri snanu

Syntax	sbstici 544
selbri stici

Syntax	sbstuna 545
selbri stuna

Axiom	ax-berti-snanu 546	Northward and southward are opposite.
⊢ go ko'a berti ko'e ko'i gi ko'e snanu ko'a ko'i

Axiom	ax-stici-stuna 547	Westward and eastward are opposite.
⊢ go ko'a stici ko'e ko'i gi ko'e stuna ko'a ko'i

5.2 Three-dimensional Euclidean space

5.2.1 Spatial directions

Syntax	sbcrane 548
selbri crane

Syntax	sbtrixe 549
selbri trixe

Syntax	sbzunle 550
selbri zunle

Syntax	sbpritu 551
selbri pritu

Syntax	sbgapru 552
selbri gapru

Syntax	sbcnita 553
selbri cnita

Axiom	ax-crane-trixe 554	Forward and backward are opposite.
⊢ go ko'a crane ko'e ko'i gi ko'e trixe ko'a ko'i

Axiom	ax-zunle-pritu 555	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 556	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 557
selbri cabna

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

5.3.2 {xlane}

Syntax	sbxlane 559
selbri xlane

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

5.3.3 {balvi}, {purci}

Syntax	sbbalvi 561
selbri balvi

Syntax	sbpurci 562
selbri purci

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

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

Theorem	kihirnihi-kinra 567	{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 568	{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 569
selbri ki'irkanxe

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

Definition	df-kihirvlina 572*	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 Functions I

6.2.1 {fancu}

Syntax	sbfancu 573
selbri fancu

Definition	df-fancu 574*	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 575*	Inference form of df-fancu 574 (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 576*	Inference form of df-fancu 574 (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.2.2 {pagyfancu}

Syntax	sbpagyfancu 577
selbri pagyfancu

Definition	df-pagyfancu 578*	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.3 Assorted claims

6.3.1 {mapti}

Syntax	sbmapti 579
selbri mapti

Definition	df-mapti 580	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 581	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.3.2 {drata}

Syntax	sbdrata 582
selbri drata

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

6.3.3 {frica}

Syntax	sbfrica 584
selbri frica

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

6.3.4 {nenri}

Syntax	sbnenri 586
selbri nenri

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

6.3.5 {fatne}

Syntax	sbfatne 588
selbri fatne

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

6.3.6 {rinka}

Syntax	sbrinka 590
selbri rinka

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

6.4 Ontological classes

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

Syntax	sbskari 592
selbri skari

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

Definition	df-skaselbri 595*	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 596*	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.4.2 Families: {lanzu}

Syntax	sblanzu 597
selbri lanzu

Syntax	sblazmihu 598
selbri lazmi'u

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

Definition	df-lazmihu 600	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

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

< Previous Next >