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  Complex numbers
6.3  Functions I
6.4  Assorted claims
6.5  Ontological classes
6.6  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 87
1.5.2  {.anai} sjanai 93
1.5.3  {naja} sbnaja 98
1.5.4  {janai} sbjanai 104
1.5.5  {nagi'a} tnagiha 109
1.5.6  {gi'anai} tgihanai 114
1.6  Conjunctions II
1.6.1  More facts about {ge} ge-com-lem 119
1.6.2  {.e} sje 124
1.6.3  {je} sbje 128
1.6.4  {gi'e} tgihe 132
*1.7  Disjunctions: {ga}, {.a}, {ja}, {gi'a}
1.7.1  {ga} bga 137
1.7.2  {.a} sja 152
1.7.3  {ja} sbja 158
1.7.4  {gi'a} tgiha 162
1.8  Biconditionals II
1.8.1  {.o} sjo 166
1.8.2  {jo} sbjo 173
1.8.3  {gi'o} tgiho 177
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 260
1.14.2  {.onai} sjonai 266
1.14.3  {jonai} sbjonai 270
1.14.4  {gi'onai} tgihonai 274
1.15  Extra connectives
1.15.1  {ginai} bgagin 278
*PART 2  NON-LOGICAL CONNECTIVES
2.1  Sets I: {nomei}, {pamei}
2.1.1  {cmima} sbcmima 282
2.1.2  {nomei} snomei 286
2.1.3  {pamei} sbpamei 289
2.2  Subsets
2.2.1  {gripau} sbgripau 294
*2.3  Internal hom I
2.3.1  {ka} sc 303
2.3.2  {ckaji} sbckaji 305
2.3.3  {ckini} sbckini 310
2.3.4  {sefsi} sbsefsi 316
2.3.5  {simsa} sbsimsa 318
2.3.6  {dunli} sbdunli 327
2.3.7  {mintu} sbmintu 334
2.3.8  {steci} sbsteci 343
2.3.9  {mupli} sbmupli 348
2.3.10  {simxu} sbsimxu 355
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 408
2.10  Relative clauses I: {poi}, {ke'a}, {ku'o}
2.10.1  {po'u} brdpu 423
2.11  Internal hom II: {kampu}
2.11.1  {kampu} sbkampu 425
2.12  Union: {jo'e}
2.12.1  {jo'e} sjohe 429
2.13  Intersection: {ku'a}
2.13.1  {ku'a} skuha 433
*2.14  Internal bridi
2.14.1  {du'u} sdu 437
2.14.2  {bridi} sceho 438
2.14.3  {fatci} sbfatci 446
2.14.4  {nibli} sbnibli 451
2.14.5  {sigda} sbsigda 457
2.14.6  {tsida} sbtsida 459
2.14.7  {kanxe} sbkanxe 461
2.14.8  {vlina} sbvlina 463
2.14.9  {nalti} sbnalti 465
2.15  Parallel reasoning: {fa'u}
2.15.1  {fa'u} sfahu 468
2.16  Deletion: {zi'o}
*2.17  Properties of relations
2.17.1  Transitivity: {takni} sbtakni 478
2.17.2  Symmetry: {kinfi} sbkinfi 481
2.17.3  Reflexivity: {kinra} sbkinra 484
2.17.4  Euclidean: {efklipi}, {efklizu} sbefklipi 490
2.18  Existential quantifiers II: {pa da}
2.18.1  Magmas: {klojere} sbklojere 504
2.18.2  Semigroups: {kloje} sbkloje 506
2.18.3  Monoids: {sezni} sbsezni 508
*PART 3  NUMBERS
*3.1  Natural numbers
3.1.1  Zero: {li no} sli 511
3.1.2  Successor I: {bai'ei}, {kacli'e} mbaihei 514
3.1.3  Natural number predicate: {kacna'u} bkacnahu 527
3.1.4  Successor II ax-succ-succ 530
3.1.5  Addition I: {su'i} msuhi 537
3.1.6  Addition II: {sumji} bsumji 541
3.1.7  Multiplication I: {pi'i} mpihi 545
3.1.8  Multiplication II: {pilji} bpilji 548
3.1.9  Comparison I: {kacme'a} bkacmeha 552
3.2  Exponents I: {tenfa}
3.3  Logarithms: {dugri}
3.4  Cardinality
3.4.1  {ka'au} mkahau 561
3.4.2  {kazmi} sbkazmi 562
*PART 4  MEREOLOGY
4.1  Parthood
4.1.1  {pagbu} sbpagbu 567
4.1.2  {jompau} sbjompau 576
4.1.3  {kuzypau} sbkuzypau 580
PART 5  SPACE & SPACETIME
5.1  Two-dimensional Euclidean space
5.1.1  Compass directions sbberti 584
5.2  Three-dimensional Euclidean space
5.2.1  Spatial directions sbcrane 590
5.3  Minkowski spacetime
5.3.1  {cabna} sbcabna 599
5.3.2  {xlane} sbxlane 601
5.3.3  {balvi}, {purci} sbbalvi 603
PART 6  RELATIONAL LOGIC
6.1  Lattice of relations
6.1.1  {ki'irni'i} sbkihirnihi 606
6.1.2  {ki'irkanxe} sbkihirkanxe 611
6.1.3  {ki'irvlina} sbkihirvlina 613
6.2  Complex numbers
6.2.1  Complex number predicate: {lujna'u} sblujnahu 615
6.2.2  Real number predicate: {mrena'u} sbmrenahu 623
6.3  Functions I
6.3.1  {fancu} sbfancu 626
6.3.2  {pagyfancu} sbpagyfancu 630
6.4  Assorted claims
6.4.1  {mapti} sbmapti 632
6.4.2  {drata} sbdrata 635
6.4.3  {frica} sbfrica 637
6.4.4  {nenri} sbnenri 639
6.4.5  {fatne} sbfatne 641
6.4.6  {rinka} sbrinka 643
6.5  Ontological classes
*6.5.1  Colors: {skari} sbskari 645
6.5.2  Families: {lanzu} sblanzu 650
6.6  Generated baseline ontology
6.6.1  Classes of selbri ax-skaselbri-blabi 708
6.6.2  Subrelations between selbri ax-since-respa 776

< 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-800 9 801-827

< Wrap Next >