mapti-ckini - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > mapti-ckini

Theorem mapti-ckini 634

Description: Under postulated definitions of la xorxes and la korvo, {mapti} is a subrelation of {ckini}. (Contributed by la korvo, 22-Aug-2024.)

**Assertion**
Ref	Expression
mapti-ckini	⊢ ganai ko'a mapti ko'e ko'i gi ko'a ckini ko'e ko'i

Proof of Theorem mapti-ckini Dummy variable de is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mapti 633	. . 3 ⊢ go ko'a mapti ko'e ko'i gi ge ko'a ckini ko'e ko'i gi ge ro de zo'u ganai de ckini ko'e ko'i gi de du ko'a gi ro de zo'u ganai ko'a ckini de ko'i gi de du ko'e
2	1	go-ganai 63	. 2 ⊢ ganai ko'a mapti ko'e ko'i gi ge ko'a ckini ko'e ko'i gi ge ro de zo'u ganai de ckini ko'e ko'i gi de du ko'a gi ro de zo'u ganai ko'a ckini de ko'i gi de du ko'e
3		ax-ge-le 43	. 2 ⊢ ganai ge ko'a ckini ko'e ko'i gi ge ro de zo'u ganai de ckini ko'e ko'i gi de du ko'a gi ro de zo'u ganai ko'a ckini de ko'i gi de du ko'e gi ko'a ckini ko'e ko'i
4	2, 3	syl 20	1 ⊢ ganai ko'a mapti ko'e ko'i gi ko'a ckini ko'e ko'i

Colors of variables: sumti selbri bridi

Syntax hints: ganai bgan 9 ge bge 42 ro brd 191 du sbdu 214 ckini sbckini 310 mapti sbmapti 632

This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 15 ax-ge-le 43

This theorem depends on definitions: df-go 61 df-mapti 633

This theorem is referenced by: (None)