HomeHome brismu bridi
Theorem List (p. 4 of 11)
< Previous  Next >

Mirrors  >  Metamath Home Page  >  Home Page  >  Theorem List Contents       This page: Page List

Theorem List for brismu bridi - 301-400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremgonaiir 301 Inference form of df-gonai 298 (Contributed by la korvo, 8-Aug-2023.)
gonai broda gi brode   =>   ⊢ naku ge broda gi brode
 
Theoremgonairi 302 Reverse inference form of df-gonai 298 (Contributed by la korvo, 8-Aug-2023.)
ge ga broda gi brode gi naku ge broda gi brode   =>   ⊢ gonai broda gi brode
 
1.14.2  {.onai}
 
Syntaxsjonai 303

sumti ko'a .onai ko'e
 
Definitiondf-onai 304 Definition of {.onai} in terms of {gonai}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14.
go ko'a .onai ko'e bo'a gi gonai ko'a bo'a gi ko'e bo'a
 
Theoremonaii 305 Inference form of df-onai 304 (Contributed by la korvo, 16-Aug-2023.)
ko'a .onai ko'e bo'a   =>   ⊢ gonai ko'a bo'a gi ko'e bo'a
 
Theoremonairi 306 Reverse inference form of df-onai 304 (Contributed by la korvo, 16-Aug-2023.)
gonai ko'a bo'a gi ko'e bo'a   =>   ⊢ ko'a .onai ko'e bo'a
 
1.14.3  {jonai}
 
Syntaxsbjonai 307*

selbri bu'a jonai bu'e
 
Definitiondf-jonai 308* Definition of {jonai} in terms of {gonai}. By analogy with example 12.2-5 of [CLL] p. 14.
go ko'a bu'a jonai bu'e ko'e gi gonai ko'a bu'a ko'e gi ko'a bu'e ko'e
 
Theoremjonaii 309* Inference form of df-jonai 308 (Contributed by la korvo, 16-Aug-2023.)
ko'a bu'a jonai bu'e ko'e   =>   ⊢ gonai ko'a bu'a ko'e gi ko'a bu'e ko'e
 
Theoremjonairi 310* Reverse inference form of df-jonai 308 (Contributed by la korvo, 16-Aug-2023.)
gonai ko'a bu'a ko'e gi ko'a bu'e ko'e   =>   ⊢ ko'a bu'a jonai bu'e ko'e
 
1.14.4  {gi'onai}
 
Syntaxtgihonai 311

brirebla bo'a gi'onai bo'e
 
Definitiondf-gihonai 312 Definition of {gi'onai} in terms of {gonai}.
go ko'a bo'a gi'onai bo'e gi gonai ko'a bo'a gi ko'a bo'e
 
Theoremgihonaii 313 Inference form of df-gihonai 312 (Contributed by la korvo, 14-Aug-2023.)
ko'a bo'a gi'onai bo'e   =>   ⊢ gonai ko'a bo'a gi ko'a bo'e
 
Theoremgihonairi 314 Inference form of df-gihonai 312 (Contributed by la korvo, 14-Aug-2023.)
gonai ko'a bo'a gi ko'a bo'e   =>   ⊢ ko'a bo'a gi'onai bo'e
 
1.15  Extra connectives
 
1.15.1  {ginai}
 
Syntaxbgagin 315

bridi ga broda ginai brode
 
Syntaxbgogin 316

bridi go broda ginai brode
 
Definitiondf-ginai-ga 317

go ga brode ginai broda gi ganai broda gi brode
 
Definitiondf-ginai-go 318

go go broda ginai brode gi gonai broda gi brode
 
PART 2  NON-LOGICAL CONNECTIVES

We build the various non-logical connectives, which express combinations of elements of relations beyond truth tables. In particular, we develop the notion of set membership.

 
2.1  Sets I: {nomei}, {pamei}
 
2.1.1  {cmima}
 
Syntaxsbcmima 319

selbri cmima
 
Syntaxsbselcmi 320

selbri selcmi
 
Definitiondf-selcmi 321

go ko'a selcmi ko'e gi ko'a se cmima ko'e
 
Axiomax-cmima-ext 322 The Axiom of Extensionality: If no elements differ in elementhood for two sets, then they are the same set.
ganai ro da zo'u da cmima ko'a .o ko'e gi ko'a du ko'e
 
2.1.2  {nomei}
 
Syntaxsnomei 323

sumti le nomei ku
 
Definitiondf-nomei 324 {le nomei} is the empty set. Literally it is the set with zero cardinality. By standard folklore of sets, it is unique up to isomorphism, justifying {le}.
naku ko'a cmima le nomei ku
 
Theoremnomei-gaiho 325 If the empty set is inhabited, then there is a contradiction. (Contributed by la korvo, 16-May-2024.)
ko'a cmima le nomei ku   =>   ⊢ gai'o
 
2.1.3  {pamei}
 
Syntaxsbpamei 326

selbri pamei
 
Definitiondf-pamei 327 The singleton set is the unique set whose elements are all isomorphic. Since we use the full semantics of second-order logic, we cannot construct the witness isomorphisms. As a compromise, we construct the isomorphism between any two elements of any particular singleton set.
go ko'a pamei ko'e .e ko'i gi ko'e du ko'i
 
Theorempameii 328 Inference form of df-pamei 327 (Contributed by la korvo, 16-May-2024.)
ko'a pamei ko'e .e ko'i   =>   ⊢ ko'e du ko'i
 
Theorempameiii 329 Inference form of df-pamei 327 (Contributed by la korvo, 16-May-2024.)
ko'a pamei ko'e   &   ⊢ ko'a pamei ko'i   =>   ⊢ ko'e du ko'i
 
Axiomax-pamei-cmima 330 The singleton set has one element.
ganai ko'a pamei ko'e gi ko'e cmima ko'a
 
2.2  Subsets
 
2.2.1  {gripau}
 
Syntaxsbgripau 331

selbri gripau
 
Definitiondf-gripau 332 Definition of {gripau} in terms of {cmima} and {na.a}. Defined in section 7 of [CLL] p. 18 based on the gloss "set-part". This definition is phrased with an implicit universal quantification instead of {ro da zo'u da cmima ko'a na.a ko'e} or {ro da poi ke'a cmima ko'a ku'o zo'u da cmima ko'e} for succinctness and ease of theorem-proving.
go ko'a gripau ko'e gi ko'i cmima ko'a na.a ko'e
 
Theoremgripaui 333 Inference form of df-gripau 332 (Contributed by la korvo, 15-Jul-2024.)
ko'a gripau ko'e   =>   ⊢ ko'i cmima ko'a na.a ko'e
 
Theoremgripauri 334 Reverse inference form of df-gripau 332 (Contributed by la korvo, 15-Jul-2024.)
ko'i cmima ko'a na.a ko'e   =>   ⊢ ko'a gripau ko'e
 
Theoremgripauis 335 Inference form of df-gripau 332 (Contributed by la korvo, 19-Jul-2024.)
ko'a gripau ko'e   =>   ⊢ ganai ko'i cmima ko'a gi ko'i cmima ko'e
 
Theoremgripauiis 336 Inference form of df-gripau 332 (Contributed by la korvo, 15-Jul-2024.)
ko'a gripau ko'e   &   ⊢ ko'i cmima ko'a   =>   ⊢ ko'i cmima ko'e
 
Theoremgripauris 337 Reverse inference form of df-gripau 332 (Contributed by la korvo, 19-Jul-2024.)
ganai ko'i cmima ko'a gi ko'i cmima ko'e   =>   ⊢ ko'a gripau ko'e
 
Theoremgripau-refl 338 {gripau} is reflexive. (Contributed by la korvo, 15-Jul-2024.)
ko'a gripau ko'a
 
Theoremgripau-trans 339 {gripau} is transitive. (Contributed by la korvo, 19-Jul-2024.)
ko'a gripau ko'e   &   ⊢ ko'e gripau ko'i   =>   ⊢ ko'a gripau ko'i
 
2.3  Internal hom I

The internal hom is the syntax which internalizes relations. We define {ka} abstractions as well as several useful gismu for accessing the contents of those abstractions. Our approach uses {pa ka} quantification in acknowledgement of isomorphism-invariance.

 
2.3.1  {ka}
 
Syntaxsc 340

sumti ce'u
 
Syntaxspk 341 If {bo'a} is a brirebla, then filling its first place with a sumti and wrapping it with {pa ka} yields sumti.
sumti pa ka ko'a bo'a kei
 
2.3.2  {ckaji}
 
Syntaxsbckaji 342

selbri ckaji
 
Theorembckaji 343 {ckaji} is often found with this conjugation. (Contributed by la korvo, 14-Aug-2023.)
bridi ko'a ckaji pa ka ce'u bo'a kei
 
Definitiondf-ckaji 344 Definition of {ckaji} from {ka}. Based on example 4.1-2 of [CLL] p. 11.
go ko'a ckaji pa ka ce'u bo'a kei gi ko'a bo'a
 
Theoremckajii 345 Inference form of df-ckaji 344 (Contributed by la korvo, 17-Jul-2023.)
ko'a ckaji pa ka ce'u bo'a kei   =>   ⊢ ko'a bo'a
 
Theoremckajiri 346 Reverse inference form of df-ckaji 344 (Contributed by la korvo, 17-Jul-2023.)
ko'a bo'a   =>   ⊢ ko'a ckaji pa ka ce'u bo'a kei
 
2.3.3  {ckini}
 
Syntaxsbckini 347

selbri ckini
 
Theorembckini 348 {ckini} is often found with this conjugation. (Contributed by la korvo, 14-Aug-2023.)
bridi ko'a ckini ko'e pa ka ce'u bu'a ce'u kei
 
Definitiondf-ckini 349

go ko'a ckini ko'e pa ka ce'u bu'a ce'u kei gi ko'a bu'a ko'e
 
Theoremckinii 350 Inference form of df-ckini 349 (Contributed by la korvo, 17-Jul-2023.)
ko'a ckini ko'e pa ka ce'u bu'a ce'u kei   =>   ⊢ ko'a bu'a ko'e
 
Theoremckiniri 351 Reverse inference form of df-ckini 349 (Contributed by la korvo, 17-Jul-2023.)
ko'a bu'a ko'e   =>   ⊢ ko'a ckini ko'e pa ka ce'u bu'a ce'u kei
 
Theoremckini-se 352 {se} can be inserted underneath ckini3. Example theorem from early draft of la brismu. (Contributed by la korvo, 12-Jul-2023.)
ko'a ckini ko'e pa ka ce'u bu'a ce'u kei   =>   ⊢ ko'e ckini ko'a pa ka ce'u se bu'a ce'u kei
 
2.3.4  {sefsi}
 
Syntaxsbsefsi 353

selbri sefsi
 
Definitiondf-sefsi 354 A useful experimental gismu like {ckini}. In particular, {sefsi} can adapt between unary and binary {ka} abstractions. This definition was given by la xorxes.
go ko'a sefsi ko'e gi ko'a ckini ko'a ko'e
 
2.3.5  {simsa}
 
Syntaxsbsimsa 355

selbri simsa
 
Theorembsimsa 356 {simsa} is often found with this conjugation. (Contributed by la korvo, 6-Aug-2023.)
bridi ko'a simsa ko'e pa ka ce'u bu'a kei
 
Definitiondf-simsa 357 Definition of {simsa} in terms of {ckaji}.
go ko'a simsa ko'e ko'i gi ko'a .e ko'e ckaji ko'i
 
Theoremsimsai 358 Inference form of df-simsa 357 (Contributed by la korvo, 6-Aug-2023.)
ko'a simsa ko'e ko'i   =>   ⊢ ko'a .e ko'e ckaji ko'i
 
Theoremsimsail 359 Inference form of df-simsa 357 (Contributed by la korvo, 6-Aug-2023.)
ko'a simsa ko'e ko'i   =>   ⊢ ko'a ckaji ko'i
 
Theoremsimsair 360 Inference form of df-simsa 357 (Contributed by la korvo, 6-Aug-2023.)
ko'a simsa ko'e ko'i   =>   ⊢ ko'e ckaji ko'i
 
Theoremsimsari 361 Reverse inference form of df-simsa 357 (Contributed by la korvo, 6-Aug-2023.)
ko'a .e ko'e ckaji ko'i   =>   ⊢ ko'a simsa ko'e ko'i
 
Theoremsimsarii 362 Reverse inference form of df-simsa 357 (Contributed by la korvo, 6-Aug-2023.)
ko'a ckaji ko'i   &   ⊢ ko'e ckaji ko'i   =>   ⊢ ko'a simsa ko'e ko'i
 
Axiomax-simsa-sym 363 {simsa} is symmetric.
go ko'a simsa ko'e ko'i gi ko'e simsa ko'a ko'i
 
2.3.6  {dunli}
 
Syntaxsbdunli 364

selbri dunli
 
Theorembdunli 365 {dunli} is often found with this conjugation. (Contributed by la korvo, 23-Jun-2024.)
bridi ko'a dunli ko'e pa ka ce'u bu'a ce'u kei
 
Definitiondf-dunli 366 Definition of {dunli} by la ilmen in terms of {ckini}. A metavariable is used instead of a universal quantifier to ease manipulation.
go ko'a dunli ko'e ko'i gi ko'a .o ko'e ckini ko'o ko'i
 
Theoremdunlii 367 Inference form of df-dunli 366 (Contributed by la korvo, 23-Jun-2024.)
ko'a dunli ko'e ko'i   =>   ⊢ ko'a .o ko'e ckini ko'o ko'i
 
Theoremdunliri 368 Reverse inference form of df-dunli 366 (Contributed by la korvo, 23-Jun-2024.)
ko'a .o ko'e ckini ko'o ko'i   =>   ⊢ ko'a dunli ko'e ko'i
 
Theoremdunli-refl 369 {dunli} is reflexive over any dunli3. (Contributed by la korvo, 14-Aug-2024.)
ko'a dunli ko'a ko'e
 
Theoremdunli-sym 370 Because modal x1 and modal x2 of {dunli} are definitionally interchangeable, {dunli} itself is symmetric. (Contributed by la korvo, 20-Sep-2024.)
go ko'a dunli ko'e ko'i gi ko'e dunli ko'a ko'i
 
2.3.7  {mintu}
 
Syntaxsbmintu 371

selbri mintu
 
Theorembmintu 372 {mintu} is often found with this conjugation. (Contributed by la korvo, 6-Aug-2023.)
bridi ko'a mintu ko'e pa ka ce'u bu'a kei
 
Definitiondf-mintu 373 Definition of {mintu} in terms of {ckaji}.
go ko'a mintu ko'e ko'i gi ko'a .o ko'e ckaji ko'i
 
Theoremmintui 374 Inference form of df-mintu 373 (Contributed by la korvo, 6-Aug-2023.)
ko'a mintu ko'e ko'i   =>   ⊢ ko'a .o ko'e ckaji ko'i
 
Theoremminturi 375 Reverse inference form of df-mintu 373 (Contributed by la korvo, 6-Aug-2023.)
ko'a .o ko'e ckaji ko'i   =>   ⊢ ko'a mintu ko'e ko'i
 
Theoremmintu-refl 376 {mintu} is reflexive over any mintu3. (Contributed by la korvo, 14-Aug-2024.)
ko'a mintu ko'a ko'e
 
Theoremmintu-sym 377 Because x1 and x2 of {mintu} are definitionally interchangeable, it is symmetric. (Contributed by la korvo, 20-Sep-2024.)
go ko'a mintu ko'e ko'i gi ko'e mintu ko'a ko'i
 
Theoremdu-mintu 378 Suggested by baseline definition of {mintu}: {du} is {mintu} without a standard of comparison, which is a stronger condition. (Contributed by la korvo, 25-Jun-2024.)
ko'a du ko'e   =>   ⊢ ko'a mintu ko'e ko'i
 
Theoremsimsa-mintu 379 {simsa} implies {mintu}. (Contributed by la korvo, 25-Jun-2024.)
ko'a simsa ko'e ko'i   =>   ⊢ ko'a mintu ko'e ko'i
 
2.3.8  {steci}
 
Syntaxsbsteci 380

selbri steci
 
Definitiondf-steci 381 Definition of {steci} in terms of {ckaji} and {cmima}.
go ko'a steci ko'e ko'i gi ge ko'e ckaji ko'a gi ko'e cmima ko'i
 
Theoremstecii 382 Inference form of df-steci 381 (Contributed by la korvo, 17-Aug-2023.)
ko'a steci ko'e ko'i   =>   ⊢ ge ko'e ckaji ko'a gi ko'e cmima ko'i
 
Theoremsteciri 383 Reverse inference form of df-steci 381 (Contributed by la korvo, 17-Aug-2023.)
ge ko'e ckaji ko'a gi ko'e cmima ko'i   =>   ⊢ ko'a steci ko'e ko'i
 
Theoremstecirii 384 Reverse inference form of df-steci 381 (Contributed by la korvo, 17-Aug-2023.)
ko'e ckaji ko'a   &   ⊢ ko'e cmima ko'i   =>   ⊢ ko'a steci ko'e ko'i
 
2.3.9  {mupli}
 
Syntaxsbmupli 385

selbri mupli
 
Definitiondf-mupli 386 Tentative definition of {mupli}. It is worth noting that there is currently a lack of community consensus on whether all elements of mupli3 must satisfy mupli2.
go ko'a mupli ko'e ko'i gi ge ko'a ckaji ko'e gi ko'a cmima ko'i
 
Theoremmuplii 387 Inference form of df-mupli 386 (Contributed by la korvo, 23-Aug-2023.)
ko'a mupli ko'e ko'i   =>   ⊢ ge ko'a ckaji ko'e gi ko'a cmima ko'i
 
Theoremmuplili 388 Inference form of df-mupli 386 (Contributed by la korvo, 23-Aug-2023.)
ko'a mupli ko'e ko'i   =>   ⊢ ko'a ckaji ko'e
 
Theoremmupliiri 389 Inference form of df-mupli 386 (Contributed by la korvo, 23-Aug-2023.)
ko'a mupli ko'e ko'i   =>   ⊢ ko'a cmima ko'i
 
Theoremmupliri 390 Reverse inference form of df-mupli 386 (Contributed by la korvo, 23-Aug-2023.)
ge ko'a ckaji ko'e gi ko'a cmima ko'i   =>   ⊢ ko'a mupli ko'e ko'i
 
Theoremmuplirii 391 Reverse inference form of df-mupli 386 (Contributed by la korvo, 23-Aug-2023.)
ko'a ckaji ko'e   &   ⊢ ko'a cmima ko'i   =>   ⊢ ko'a mupli ko'e ko'i
 
2.3.10  {simxu}
 
Syntaxsbsimxu 392

selbri simxu
 
Definitiondf-simxu 393* An alternate definition of {simxu} which doesn't use {poi ke'a cmima} for element selection.
go ko'a simxu ko'e gi ro da zo'u ro de zo'u ganai da .e de cmima ko'a gi da ckini de ko'e
 
Theoremsimxui 394* Inference form of df-simxu 393 (Contributed by la korvo, 23-Aug-2023.)
ko'a simxu ko'e   =>   ⊢ ro da zo'u ro de zo'u ganai da .e de cmima ko'a gi da ckini de ko'e
 
Theoremsimxuri 395* Reverse inference form of df-simxu 393 (Contributed by la korvo, 23-Aug-2023.)
ro da zo'u ro de zo'u ganai da .e de cmima ko'a gi da ckini de ko'e   =>   ⊢ ko'a simxu ko'e
 
2.4  Conversion II: {te}
 
Syntaxsbt 396 If {bu'a} is a selbri, then so is {te bu'a}.
selbri te bu'a
 
Definitiondf-te 397 Definition of {te} as a swap of terbri.
go ko'i te bu'a ko'e ko'a gi ko'a bu'a ko'e ko'i
 
Theoremtei 398 Inference form of df-te 397 (Contributed by la korvo, 18-Jul-2023.)
ko'i te bu'a ko'e ko'a   =>   ⊢ ko'a bu'a ko'e ko'i
 
Theoremteri 399 Reverse inference form of df-te 397 (Contributed by la korvo, 18-Jul-2023.)
ko'a bu'a ko'e ko'i   =>   ⊢ ko'i te bu'a ko'e ko'a
 
Theoremte-invo 400 {te} is an involution. (Contributed by la korvo, 18-Jul-2023.)
ko'a te te bu'a ko'e ko'i   =>   ⊢ ko'a bu'a ko'e ko'i
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300301-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 < Previous  Next >