P. 8 of Theorem List - brismu bridi

Home	brismu bridi Theorem List (p. 8 of 11)	< Previous Next >
		Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List

**Theorem List for brismu bridi -** 701-800 *Has distinct variable group(s)
Type	Label	Description
Statement

6.3 Functions I

6.3.1 {fancu}

Syntax	sbfancu 701
selbri fancu

Definition	df-fancu 702*	Definition of {fancu}. Note that the name of the function is neither unique nor concrete.
⊢ go ko'a fancu ko'e ko'i ko'o gi ro da poi ke'a cmima ko'e ku'o zo'u pa de zo'u ge de cmima ko'i gi da ckini de ko'o

Theorem	fancui 703*	Inference form of df-fancu 702 (Contributed by la korvo, 12-Aug-2024.)
⊢ ko'a fancu ko'e ko'i ko'o ⊢ ro da poi ke'a cmima ko'e ku'o zo'u pa de zo'u ge de cmima ko'i gi da ckini de ko'o

Theorem	fancuii 704*	Inference form of df-fancu 702 (Contributed by la korvo, 12-Aug-2024.)
⊢ ko'a fancu ko'e ko'i ko'o ⊢ de cmima ko'e ⊢ pa da zo'u ge da cmima ko'i gi de ckini da ko'o

6.3.2 {pagyfancu}

Syntax	sbpagyfancu 705
selbri pagyfancu

Definition	df-pagyfancu 706*	Definition of {pagyfancu} in terms of {ki'irni'i}.
⊢ go su'o da zo'u su'o de zo'u su'o di zo'u da pagyfancu de di pa ka ce'u bu'a ce'u kei gi pa ka su'o da zo'u ce'u .e ce'u bu'a da kei ki'irni'i pa ka ce'u du ce'u kei

6.4 Assorted claims

6.4.1 {mapti}

Syntax	sbmapti 707
selbri mapti

Definition	df-mapti 708	Proposed definition of {mapti} as a witness to an inhabited bijection.
⊢ go ko'a mapti ko'e ko'i gi ge ko'a ckini ko'e ko'i gi ge ro da zo'u ganai da ckini ko'e ko'i gi da du ko'a gi ro da zo'u ganai ko'a ckini da ko'i gi da du ko'e

Theorem	mapti-ckini 709	Under postulated definitions of la xorxes and la korvo, {mapti} is a subrelation of {ckini}. (Contributed by la korvo, 22-Aug-2024.)
⊢ ganai ko'a mapti ko'e ko'i gi ko'a ckini ko'e ko'i

6.4.2 {drata}

Syntax	sbdrata 710
selbri drata

Axiom	ax-drata-irrefl 711	{drata} is irreflexive.
⊢ naku ko'a drata ko'a ko'e

6.4.3 {frica}

Syntax	sbfrica 712
selbri frica

Axiom	ax-frica-irrefl 713	{frica} is irreflexive.
⊢ naku ko'a frica ko'a ko'e

6.4.4 {nenri}

Syntax	sbnenri 714
selbri nenri

Axiom	ax-nenri-trans 715	{nenri} is transitive.
⊢ ganai ge ko'a nenri ko'e gi ko'e nenri ko'i gi ko'a nenri ko'i

6.4.5 {fatne}

Syntax	sbfatne 716
selbri fatne

Axiom	ax-fatne-sym 717	{fatne} is symmetric.
⊢ go ko'a fatne ko'e gi ko'e fatne ko'a

6.4.6 {rinka}

Syntax	sbrinka 718
selbri rinka

Axiom	ax-rinka-balvi 719	Physical causation implies spatiotemporal causation.
⊢ ganai ko'a rinka ko'e ko'i gi ko'a balvi ko'e

6.5 Ontological classes

6.5.1 Colors: {skari} The schema for colors classifies one type, the colors ({skaselbri}).

Syntax	sbskari 720
selbri skari

Axiom	ax-skari-ckaji 721	Colors are extensionally defined in terms of {skari}.
⊢ ganai ko'a skari ko'e ko'i ko'o gi ko'a ckaji ko'e

Syntax	sbska 722	All {skaselbri} are {selbri}.
skaselbri bu'a selbri bu'a

Definition	df-skaselbri 723*	To be colored is to appear colored in a certain context.
skaselbri bu'a ⊢ go ko'a bu'a gi su'o da zo'u su'o de zo'u ko'a skari pa ka ce'u bu'a kei da de

Axiom	ax-xinmo2-skari2 724*	Definitionally, xinmo2 is drawn from skari2.
⊢ ganai ko'a se xinmo ko'e gi su'o da zo'u su'o de zo'u su'o di zo'u ko'a se skari da de di

6.5.2 Families: {lanzu}

Syntax	sblanzu 725
selbri lanzu

Syntax	sblazmihu 726
selbri lazmi'u

Axiom	ax-lanzu-cmima 727	{lanzu} is a subrelation of {cmima} as implied by df-lazmihu 728 and baseline notes.
⊢ ganai ko'a lanzu ko'e ko'i gi ko'e cmima ko'a

Definition	df-lazmihu 728	Definition of {lazmi'u} in terms of {lanzu} and {cmima} from the baseline notes.
⊢ go ko'a lazmi'u ko'e gi su'o da poi ke'a lanzu ku'o zo'u ko'a mintu ko'e pa ka ce'u cmima da kei

6.6 Generated baseline ontology

Syntax	sbbakni 729	### Generated baseline ontology ###
selbri bakni

Syntax	sbbambu 730
selbri bambu

Syntax	sbbanfi 731
selbri banfi

Syntax	sbbifce 732
selbri bifce

Syntax	sbcindu 733
selbri cindu

Syntax	sbcinfo 734
selbri cinfo

Syntax	sbcinki 735
selbri cinki

Syntax	sbcipni 736
selbri cipni

Syntax	sbcivla 737
selbri civla

Syntax	sbckunu 738
selbri ckunu

Syntax	sbcribe 739
selbri cribe

Syntax	sbcurnu 740
selbri curnu

Syntax	sbdanlu 741
selbri danlu

Syntax	sbdatka 742
selbri datka

Syntax	sbfinpe 743
selbri finpe

Syntax	sbgerku 744
selbri gerku

Syntax	sbgunse 745
selbri gunse

Syntax	sbjalra 746
selbri jalra

Syntax	sbjipci 747
selbri jipci

Syntax	sbjukni 748
selbri jukni

Syntax	sbkanba 749
selbri kanba

Syntax	sbkumte 750
selbri kumte

Syntax	sblabno 751
selbri labno

Syntax	sblanme 752
selbri lanme

Syntax	sblelxe 753
selbri lelxe

Syntax	sblorxu 754
selbri lorxu

Syntax	sbmabru 755
selbri mabru

Syntax	sbmanti 756
selbri manti

Syntax	sbmarna 757
selbri marna

Syntax	sbmirli 758
selbri mirli

Syntax	sbmlatu 759
selbri mlatu

Syntax	sbnimre 760
selbri nimre

Syntax	sbpoplu 761
selbri poplu

Syntax	sbractu 762
selbri ractu

Syntax	sbratcu 763
selbri ratcu

Syntax	sbremna 764
selbri remna

Syntax	sbrespa 765
selbri respa

Syntax	sbrozgu 766
selbri rozgu

Syntax	sbsfani 767
selbri sfani

Syntax	sbsince 768
selbri since

Syntax	sbsluni 769
selbri sluni

Syntax	sbsmacu 770
selbri smacu

Syntax	sbsmani 771
selbri smani

Syntax	sbspati 772
selbri spati

Syntax	sbsrasu 773
selbri srasu

Syntax	sbtirxu 774
selbri tirxu

Syntax	sbtoldi 775
selbri toldi

Syntax	sbtujli 776
selbri tujli

Syntax	sbxanto 777
selbri xanto

Syntax	sbxarju 778
selbri xarju

Syntax	sbxasli 779
selbri xasli

Syntax	sbxirma 780
selbri xirma

Syntax	sbxruba 781
selbri xruba

Syntax	sbxruki 782
selbri xruki

6.6.1 Classes of selbri

Axiom	ax-kluselbri-baxso 783	Automatically generated axiom: {baxso} is {kluselbri}
kluselbri baxso

Axiom	ax-kluselbri-bengo 784	Automatically generated axiom: {bengo} is {kluselbri}
kluselbri bengo

Axiom	ax-kluselbri-bemro 785	Automatically generated axiom: {bemro} is {kluselbri}
kluselbri bemro

Axiom	ax-kluselbri-bindo 786	Automatically generated axiom: {bindo} is {kluselbri}
kluselbri bindo

Axiom	ax-kluselbri-brazo 787	Automatically generated axiom: {brazo} is {kluselbri}
kluselbri brazo

Axiom	ax-kluselbri-brito 788	Automatically generated axiom: {brito} is {kluselbri}
kluselbri brito

Axiom	ax-kluselbri-budjo 789	Automatically generated axiom: {budjo} is {kluselbri}
kluselbri budjo

Axiom	ax-kluselbri-dadjo 790	Automatically generated axiom: {dadjo} is {kluselbri}
kluselbri dadjo

Axiom	ax-kluselbri-dotco 791	Automatically generated axiom: {dotco} is {kluselbri}
kluselbri dotco

Axiom	ax-kluselbri-dzipo 792	Automatically generated axiom: {dzipo} is {kluselbri}
kluselbri dzipo

Axiom	ax-kluselbri-filso 793	Automatically generated axiom: {filso} is {kluselbri}
kluselbri filso

Axiom	ax-kluselbri-fraso 794	Automatically generated axiom: {fraso} is {kluselbri}
kluselbri fraso

Axiom	ax-kluselbri-friko 795	Automatically generated axiom: {friko} is {kluselbri}
kluselbri friko

Axiom	ax-kluselbri-gento 796	Automatically generated axiom: {gento} is {kluselbri}
kluselbri gento

Axiom	ax-kluselbri-glico 797	Automatically generated axiom: {glico} is {kluselbri}
kluselbri glico

Axiom	ax-kluselbri-jegvo 798	Automatically generated axiom: {jegvo} is {kluselbri}
kluselbri jegvo

Axiom	ax-kluselbri-jerxo 799	Automatically generated axiom: {jerxo} is {kluselbri}
kluselbri jerxo

Axiom	ax-kluselbri-jordo 800	Automatically generated axiom: {jordo} is {kluselbri}
kluselbri jordo

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

< Previous Next >