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 ku gi pa ka su'o da zo'u ce'u .e ce'u bu'a da ku ki'irni'i pa ka ce'u du ce'u ku

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

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	sbgumri 745
selbri gumri

Syntax	sbgunse 746
selbri gunse

Syntax	sbjalra 747
selbri jalra

Syntax	sbjipci 748
selbri jipci

Syntax	sbjukni 749
selbri jukni

Syntax	sbkanba 750
selbri kanba

Syntax	sbkuhurkupresu 751
selbri ku'urkupresu

Syntax	sbkumte 752
selbri kumte

Syntax	sblabno 753
selbri labno

Syntax	sblanme 754
selbri lanme

Syntax	sblelxe 755
selbri lelxe

Syntax	sblorxu 756
selbri lorxu

Syntax	sbmabru 757
selbri mabru

Syntax	sbmanti 758
selbri manti

Syntax	sbmarna 759
selbri marna

Syntax	sbmirli 760
selbri mirli

Syntax	sbmlatu 761
selbri mlatu

Syntax	sbmledi 762
selbri mledi

Syntax	sbnimre 763
selbri nimre

Syntax	sbpoplu 764
selbri poplu

Syntax	sbractu 765
selbri ractu

Syntax	sbratcu 766
selbri ratcu

Syntax	sbremna 767
selbri remna

Syntax	sbrespa 768
selbri respa

Syntax	sbrozgu 769
selbri rozgu

Syntax	sbsfani 770
selbri sfani

Syntax	sbsince 771
selbri since

Syntax	sbsluni 772
selbri sluni

Syntax	sbsmacu 773
selbri smacu

Syntax	sbsmani 774
selbri smani

Syntax	sbspati 775
selbri spati

Syntax	sbsrasu 776
selbri srasu

Syntax	sbtirxu 777
selbri tirxu

Syntax	sbtoldi 778
selbri toldi

Syntax	sbtujli 779
selbri tujli

Syntax	sbxanto 780
selbri xanto

Syntax	sbxarju 781
selbri xarju

Syntax	sbxasli 782
selbri xasli

Syntax	sbxirma 783
selbri xirma

Syntax	sbxruba 784
selbri xruba

Syntax	sbxruki 785
selbri xruki

6.6.1 Classes of selbri

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

< Previous Next >