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  Sets I: {nomei}, {pamei}
1.15  Mutual exclusion I
1.16  Extra connectives
PART 2  NON-LOGICAL CONNECTIVES
2.1  Internal hom I
2.2  Conversion II: {te}
2.3  Pairing: {ce}
2.4  Existential quantifiers I: {su'o}
2.5  Relative clauses I: {poi}, {ke'a}, {ku'o}
2.6  Internal hom II: {kampu}
2.7  Union: {jo'e}
2.8  Intersection: {ku'a}
2.9  Internal bridi
PART 3  NUMBERS
3.1  Natural numbers
3.2  Existential quantifiers II: {pa da}
3.3  Logarithms: {dugri}
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  Open classes of relations
6.2  Lattice of relations
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 69
1.5.2  {.anai} sjanai 74
1.5.3  {naja} sbnaja 79
1.5.4  {janai} sbjanai 84
1.5.5  {nagi'a} tnagiha 89
1.5.6  {gi'anai} tgihanai 94
1.6  Conjunctions II
1.6.1  More facts about {ge} ge-com-lem 99
1.6.2  {.e} sje 101
1.6.3  {je} sbje 105
1.6.4  {gi'e} tgihe 109
*1.7  Disjunctions: {ga}, {.a}, {ja}, {gi'a}
1.7.1  {ga} bga 114
1.7.2  {.a} sja 124
1.7.3  {ja} sbja 130
1.7.4  {gi'a} tgiha 134
1.8  Biconditionals II
1.8.1  {.o} sjo 138
1.8.2  {jo} sbjo 144
1.8.3  {gi'o} tgiho 148
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  Sets I: {nomei}, {pamei}
1.14.1  {cmima} sbcmima 191
1.14.2  {nomei} snomei 192
1.14.3  {pamei} sbpamei 195
*1.15  Mutual exclusion I
1.15.1  {gonai} bgon 200
1.15.2  {.onai} sjonai 206
1.15.3  {jonai} sbjonai 210
1.15.4  {gi'onai} tgihonai 214
1.16  Extra connectives
1.16.1  {ginai} bgagin 218
*PART 2  NON-LOGICAL CONNECTIVES
*2.1  Internal hom I
2.1.1  {ka} sc 222
2.1.2  {ckaji} sbckaji 224
2.1.3  {ckini} sbckini 229
2.1.4  {simsa} sbsimsa 235
2.1.5  {steci} sbsteci 244
2.1.6  {mupli} sbmupli 249
2.1.7  {simxu} sbsimxu 256
2.2  Conversion II: {te}
2.3  Pairing: {ce}
2.4  Existential quantifiers I: {su'o}
2.5  Relative clauses I: {poi}, {ke'a}, {ku'o}
2.6  Internal hom II: {kampu}
2.6.1  {kampu} sbkampu 285
2.7  Union: {jo'e}
2.7.1  {jo'e} sjohe 289
2.8  Intersection: {ku'a}
2.8.1  {ku'a} skuha 293
*2.9  Internal bridi
2.9.1  {du'u} sdu 297
2.9.2  {bridi} sceho 298
2.9.3  {fatci} sbfatci 306
2.9.4  {nibli} sbnibli 311
2.9.5  {sigda} sbsigda 313
2.9.6  {tsida} sbtsida 315
2.9.7  {kanxe} sbkanxe 317
2.9.8  {vlina} sbvlina 319
*PART 3  NUMBERS
3.1  Natural numbers
3.1.1  {kacna'u} bkacnahu 321
3.1.2  {kacli'e} bkaclihe 324
3.1.3  {sumji} bsumji 337
3.1.4  {su'i} sli 340
3.1.5  {pilji} bpilji 345
3.1.6  {pi'i} mpihi 348
3.2  Existential quantifiers II: {pa da}
3.3  Logarithms: {dugri}
*PART 4  MEREOLOGY
4.1  Parthood
4.1.1  {pagbu} sbpagbu 362
4.1.2  {jompau} sbjompau 370
4.1.3  {kuzypau} sbkuzypau 374
PART 5  SPACE & SPACETIME
5.1  Two-dimensional Euclidean space
5.1.1  Compass directions sbberti 378
5.2  Three-dimensional Euclidean space
5.2.1  Spatial directions sbcrane 384
5.3  Minkowski spacetime
5.3.1  {cabna} sbcabna 393
5.3.2  {xlane} sbxlane 395
5.3.3  {balvi}, {purci} sbbalvi 397
PART 6  RELATIONAL LOGIC
*6.1  Open classes of relations
6.1.1  Transitivity: {takni} sbtakni 400
6.1.2  Symmetry: {kinfi} sbkinfi 402
6.1.3  Reflexivity: {kinra} sbkinra 404
6.1.4  Euclidean: {efklipi}, {efklizu} sbefklipi 406
6.2  Lattice of relations
6.2.1  {ki'irni'i} sbkihirnihi 410
6.2.2  {ki'irkanxe} sbkihirkanxe 413
6.2.3  {ki'irvlina} sbkihirvlina 415
6.3  Functions I
6.3.1  {pagyfancu} sbpagyfancu 417
6.4  Assorted claims
6.4.1  {mapti} sbmapti 419
6.4.2  {dunli} sbdunli 421
6.4.3  {mintu} sbmintu 423
6.4.4  {drata} sbdrata 425
6.4.5  {frica} sbfrica 427
6.4.6  {nenri} sbnenri 429
6.4.7  {fatne} sbfatne 431
6.4.8  {rinka} sbrinka 433
6.5  Ontological classes
*6.5.1  Colors: {skari} sbskari 435
6.6  Generated baseline ontology
6.6.1  Classes of selbri ax-skaselbri-blabi 494
6.6.2  Subrelations between selbri ax-since-respa 508

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

< Wrap Next >