TOC of Theorem List - brismu bridi

Home	brismu bridi Theorem List (Table of Contents)	< Wrap Next >
		Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Detailed Table of Contents Page List

Table of Contents Summary PART 1  LOGICAL CONNECTIVES
1.1  Basic syntax
1.2  Implication I: {ganai}
1.3  Conjunctions I: {ge}
1.4  Biconditionals I: {go}
1.5  Implication II
1.6  Conjunctions II
1.7  Disjunctions: {ga}, {.a}, {ja}, {gi'a}
1.8  Biconditionals II
1.9  Conversion I: {se}
1.10  Universal quantifiers I: {ro}
1.11  Identity: {du}
1.12  Boolean predicates: {cei'i}
1.13  Negation I: {gai'o}, {naku}
1.14  Mutual exclusion I
1.15  Extra connectives
PART 2  NON-LOGICAL CONNECTIVES
2.1  Sets I: {nomei}, {pamei}
2.2  Subsets
2.3  Internal hom I
2.4  Conversion II: {te}
2.5  Pairing: {ce}
2.6  Existential quantifiers I: {su'o}
2.7  Substitution
2.8  Not-free quantification
2.9  Sets II: {zilcmi}
2.10  Relative clauses I: {poi}, {ke'a}, {ku'o}
2.11  Internal hom II: {kampu}
2.12  Union: {jo'e}
2.13  Intersection: {ku'a}
2.14  Internal bridi
2.15  Parallel reasoning: {fa'u}
2.16  Deletion: {zi'o}
2.17  Properties of relations
2.18  Existential quantifiers II: {pa da}
PART 3  NUMBERS
3.1  Natural numbers
3.2  Exponents I: {tenfa}
3.3  Logarithms: {dugri}
3.4  Cardinality
PART 4  MEREOLOGY
4.1  Parthood
PART 5  SPACE & SPACETIME
5.1  Two-dimensional Euclidean space
5.2  Three-dimensional Euclidean space
5.3  Minkowski spacetime
PART 6  RELATIONAL LOGIC
6.1  Lattice of relations
6.2  Functions I
6.3  Assorted claims
6.4  Ontological classes
6.5  Generated baseline ontology

Detailed Table of Contents
(* means the section header has a description) *PART 1  LOGICAL CONNECTIVES
*1.1  Basic syntax
*1.2  Implication I: {ganai}
1.3  Conjunctions I: {ge}
1.4  Biconditionals I: {go}
*1.5  Implication II
1.5.1  {na.a} sjnaa 77
1.5.2  {.anai} sjanai 83
1.5.3  {naja} sbnaja 88
1.5.4  {janai} sbjanai 94
1.5.5  {nagi'a} tnagiha 99
1.5.6  {gi'anai} tgihanai 104
1.6  Conjunctions II
1.6.1  More facts about {ge} ge-com-lem 109
1.6.2  {.e} sje 114
1.6.3  {je} sbje 118
1.6.4  {gi'e} tgihe 122
*1.7  Disjunctions: {ga}, {.a}, {ja}, {gi'a}
1.7.1  {ga} bga 127
1.7.2  {.a} sja 138
1.7.3  {ja} sbja 144
1.7.4  {gi'a} tgiha 148
1.8  Biconditionals II
1.8.1  {.o} sjo 152
1.8.2  {jo} sbjo 159
1.8.3  {gi'o} tgiho 163
1.9  Conversion I: {se}
1.10  Universal quantifiers I: {ro}
1.11  Identity: {du}
1.12  Boolean predicates: {cei'i}
*1.13  Negation I: {gai'o}, {naku}
*1.14  Mutual exclusion I
1.14.1  {gonai} bgon 224
1.14.2  {.onai} sjonai 230
1.14.3  {jonai} sbjonai 234
1.14.4  {gi'onai} tgihonai 238
1.15  Extra connectives
1.15.1  {ginai} bgagin 242
*PART 2  NON-LOGICAL CONNECTIVES
2.1  Sets I: {nomei}, {pamei}
2.1.1  {cmima} sbcmima 246
2.1.2  {nomei} snomei 249
2.1.3  {pamei} sbpamei 252
2.2  Subsets
2.2.1  {gripau} sbgripau 257
*2.3  Internal hom I
2.3.1  {ka} sc 266
2.3.2  {ckaji} sbckaji 268
2.3.3  {ckini} sbckini 273
2.3.4  {sefsi} sbsefsi 279
2.3.5  {simsa} sbsimsa 281
2.3.6  {dunli} sbdunli 290
2.3.7  {mintu} sbmintu 297
2.3.8  {steci} sbsteci 306
2.3.9  {mupli} sbmupli 311
2.3.10  {simxu} sbsimxu 318
2.4  Conversion II: {te}
2.5  Pairing: {ce}
2.6  Existential quantifiers I: {su'o}
2.7  Substitution
2.8  Not-free quantification
2.9  Sets II: {zilcmi}
2.9.1  {zilcmi} sbzilcmi 366
2.10  Relative clauses I: {poi}, {ke'a}, {ku'o}
2.10.1  {po'u} brdpu 381
2.11  Internal hom II: {kampu}
2.11.1  {kampu} sbkampu 383
2.12  Union: {jo'e}
2.12.1  {jo'e} sjohe 387
2.13  Intersection: {ku'a}
2.13.1  {ku'a} skuha 391
*2.14  Internal bridi
2.14.1  {du'u} sdu 395
2.14.2  {bridi} sceho 396
2.14.3  {fatci} sbfatci 404
2.14.4  {nibli} sbnibli 409
2.14.5  {sigda} sbsigda 415
2.14.6  {tsida} sbtsida 417
2.14.7  {kanxe} sbkanxe 419
2.14.8  {vlina} sbvlina 421
2.14.9  {nalti} sbnalti 423
2.15  Parallel reasoning: {fa'u}
2.15.1  {fa'u} sfahu 426
2.16  Deletion: {zi'o}
*2.17  Properties of relations
2.17.1  Transitivity: {takni} sbtakni 436
2.17.2  Symmetry: {kinfi} sbkinfi 439
2.17.3  Reflexivity: {kinra} sbkinra 442
2.17.4  Euclidean: {efklipi}, {efklizu} sbefklipi 448
2.18  Existential quantifiers II: {pa da}
2.18.1  Magmas: {klojere} sbklojere 462
2.18.2  Semigroups: {kloje} sbkloje 464
2.18.3  Monoids: {sezni} sbsezni 466
*PART 3  NUMBERS
*3.1  Natural numbers
3.1.1  Zero: {li no} sli 469
3.1.2  Successor I: {bai'ei}, {kacli'e} mbaihei 472
3.1.3  Natural number predicate: {kacna'u} bkacnahu 485
3.1.4  Successor II ax-succ-succ 488
3.1.5  Addition I: {su'i} msuhi 495
3.1.6  Addition II: {sumji} bsumji 499
3.1.7  Multiplication I: {pi'i} mpihi 503
3.1.8  Multiplication II: {pilji} bpilji 506
3.1.9  Comparison I: {kacme'a} bkacmeha 510
3.2  Exponents I: {tenfa}
3.3  Logarithms: {dugri}
3.4  Cardinality
3.4.1  {ka'au} mkahau 519
3.4.2  {kazmi} sbkazmi 520
*PART 4  MEREOLOGY
4.1  Parthood
4.1.1  {pagbu} sbpagbu 525
4.1.2  {jompau} sbjompau 534
4.1.3  {kuzypau} sbkuzypau 538
PART 5  SPACE & SPACETIME
5.1  Two-dimensional Euclidean space
5.1.1  Compass directions sbberti 542
5.2  Three-dimensional Euclidean space
5.2.1  Spatial directions sbcrane 548
5.3  Minkowski spacetime
5.3.1  {cabna} sbcabna 557
5.3.2  {xlane} sbxlane 559
5.3.3  {balvi}, {purci} sbbalvi 561
PART 6  RELATIONAL LOGIC
6.1  Lattice of relations
6.1.1  {ki'irni'i} sbkihirnihi 564
6.1.2  {ki'irkanxe} sbkihirkanxe 569
6.1.3  {ki'irvlina} sbkihirvlina 571
6.2  Functions I
6.2.1  {fancu} sbfancu 573
6.2.2  {pagyfancu} sbpagyfancu 577
6.3  Assorted claims
6.3.1  {mapti} sbmapti 579
6.3.2  {drata} sbdrata 582
6.3.3  {frica} sbfrica 584
6.3.4  {nenri} sbnenri 586
6.3.5  {fatne} sbfatne 588
6.3.6  {rinka} sbrinka 590
6.4  Ontological classes
*6.4.1  Colors: {skari} sbskari 592
6.4.2  Families: {lanzu} sblanzu 597
6.5  Generated baseline ontology
6.5.1  Classes of selbri ax-skaselbri-blabi 655
6.5.2  Subrelations between selbri ax-since-respa 723

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

< Wrap Next >