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  Not-free quantification
2.8  Substitution I
2.9  Predicate Calculus
2.10  Substitution II
2.11  Sets II: {zilcmi}
2.12  Relative clauses I: {poi}, {ke'a}, {ku'o}
2.13  Internal hom II: {kampu}
2.14  Union: {jo'e}
2.15  Intersection: {ku'a}
2.16  Internal bridi
2.17  Parallel reasoning: {fa'u}
2.18  Deletion: {zi'o}
2.19  Properties of relations
2.20  Existential quantifiers II: {pa da}
2.21  Abstract algebra I: magmas, semigroups, monoids
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 109
1.5.2  {.anai} sjanai 115
1.5.3  {naja} sbnaja 120
1.5.4  {janai} sbjanai 126
1.5.5  {nagi'a} tnagiha 131
1.5.6  {gi'anai} tgihanai 136
1.6  Conjunctions II
1.6.1  More facts about {ge} ge-com-lem 141
1.6.2  {.e} sje 146
1.6.3  {je} sbje 151
1.6.4  {gi'e} tgihe 155
*1.7  Disjunctions: {ga}, {.a}, {ja}, {gi'a}
1.7.1  {ga} bga 160
1.7.2  {.a} sja 183
1.7.3  {ja} sbja 189
1.7.4  {gi'a} tgiha 193
1.8  Biconditionals II
1.8.1  {.o} sjo 197
1.8.2  {jo} sbjo 204
1.8.3  {gi'o} tgiho 208
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 297
1.14.2  {.onai} sjonai 303
1.14.3  {jonai} sbjonai 307
1.14.4  {gi'onai} tgihonai 311
1.15  Extra connectives
1.15.1  {ginai} bgagin 315
*PART 2  NON-LOGICAL CONNECTIVES
2.1  Sets I: {nomei}, {pamei}
2.1.1  {cmima} sbcmima 319
2.1.2  {nomei} snomei 323
2.1.3  {pamei} sbpamei 326
2.2  Subsets
2.2.1  {gripau} sbgripau 331
*2.3  Internal hom I
2.3.1  {ka} sc 340
2.3.2  {ckaji} sbckaji 342
2.3.3  {ckini} sbckini 347
2.3.4  {sefsi} sbsefsi 353
2.3.5  {simsa} sbsimsa 355
2.3.6  {dunli} sbdunli 364
2.3.7  {mintu} sbmintu 371
2.3.8  {steci} sbsteci 380
2.3.9  {mupli} sbmupli 385
2.3.10  {simxu} sbsimxu 392
2.4  Conversion II: {te}
2.5  Pairing: {ce}
2.6  Existential quantifiers I: {su'o}
2.7  Not-free quantification
2.8  Substitution I
2.9  Predicate Calculus
2.10  Substitution II
2.11  Sets II: {zilcmi}
2.11.1  {zilcmi} sbzilcmi 459
2.12  Relative clauses I: {poi}, {ke'a}, {ku'o}
2.12.1  {po'u} brdpu 475
2.13  Internal hom II: {kampu}
2.13.1  {kampu} sbkampu 477
2.14  Union: {jo'e}
2.14.1  {jo'e} sjohe 481
2.15  Intersection: {ku'a}
2.15.1  {ku'a} skuha 485
*2.16  Internal bridi
2.16.1  {du'u} sdu 489
2.16.2  {bridi} sceho 490
2.16.3  {fatci} sbfatci 500
2.16.4  {nibli} sbnibli 505
2.16.5  {sigda} sbsigda 511
2.16.6  {tsida} sbtsida 513
2.16.7  {kanxe} sbkanxe 515
2.16.8  {vlina} sbvlina 517
2.16.9  {nalti} sbnalti 519
2.17  Parallel reasoning: {fa'u}
2.17.1  {fa'u} sfahu 522
2.18  Deletion: {zi'o}
*2.19  Properties of relations
2.19.1  Transitivity: {takni} sbtakni 533
2.19.2  Symmetry: {kinfi} sbkinfi 536
2.19.3  Reflexivity: {kinra} sbkinra 539
2.19.4  Euclidean: {efklipi}, {efklizu} sbefklipi 545
2.20  Existential quantifiers II: {pa da}
2.20.1  Uniqueness: {pombo} sbpombo 559
2.21  Abstract algebra I: magmas, semigroups, monoids
2.21.1  Magmas: {klojere} sbklojere 563
2.21.2  Semigroups: {kloje} sbkloje 565
2.21.3  Commutative operators: {cajni} sbcajni 567
2.21.4  Monoids: {sezni} sbsezni 569
2.21.5  Groups: {dukni} sbdukni 572
*PART 3  NUMBERS
*3.1  Natural numbers
3.1.1  Zero: {li no} sli 573
3.1.2  Successor I: {bai'ei}, {kacli'e} mbaihei 576
3.1.3  Natural number predicate: {kacna'u} bkacnahu 589
3.1.4  Successor II ax-succ-succ 592
3.1.5  Addition I: {su'i} msuhi 599
3.1.6  Addition II: {sumji} bsumji 603
3.1.7  Multiplication I: {pi'i} mpihi 607
3.1.8  Multiplication II: {pilji} bpilji 610
3.1.9  Comparison I: {kacme'a} bkacmeha 614
3.2  Exponents I: {tenfa}
3.3  Logarithms: {dugri}
3.4  Cardinality
3.4.1  {ka'au} mkahau 623
3.4.2  {kazmi} sbkazmi 624
*PART 4  MEREOLOGY
4.1  Parthood
4.1.1  {pagbu} sbpagbu 629
4.1.2  {jompau} sbjompau 638
4.1.3  {kuzypau} sbkuzypau 642
PART 5  SPACE & SPACETIME
5.1  Two-dimensional Euclidean space
5.1.1  Compass directions sbberti 646
5.2  Three-dimensional Euclidean space
5.2.1  Spatial directions sbcrane 652
5.3  Minkowski spacetime
5.3.1  Events: {cfabalvi}, {mulpru} sbcfabalvi 661
5.3.2  Simultaneity: {cabna} sbcabna 665
5.3.3  Non-aorist events: {balvi}, {purci} sbbalvi 669
5.3.4  Elsewhen: {xlane} sbxlane 674
PART 6  RELATIONAL LOGIC
6.1  Lattice of relations
6.1.1  {ki'irni'i} sbkihirnihi 677
6.1.2  {ki'irdu'i} sbkihirduhi 682
6.1.3  {ki'irkanxe} sbkihirkanxe 686
6.1.4  {ki'irvlina} sbkihirvlina 688
6.2  Complex numbers
6.2.1  Complex number predicate: {lujna'u} sblujnahu 690
6.2.2  Real number predicate: {mrena'u} sbmrenahu 698
6.3  Functions I
6.3.1  {fancu} sbfancu 701
6.3.2  {pagyfancu} sbpagyfancu 705
6.4  Assorted claims
6.4.1  {mapti} sbmapti 707
6.4.2  {drata} sbdrata 710
6.4.3  {frica} sbfrica 712
6.4.4  {nenri} sbnenri 714
6.4.5  {fatne} sbfatne 716
6.4.6  {rinka} sbrinka 718
6.5  Ontological classes
*6.5.1  Colors: {skari} sbskari 720
6.5.2  Families: {lanzu} sblanzu 725
6.6  Generated baseline ontology
6.6.1  Classes of selbri ax-kluselbri-baxso 783
6.6.2  Subrelations between selbri ax-since-respa 997

< 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-900 10 901-1000 11 1001-1048

Copyright terms: Public domain

< Wrap Next >