mapti-ckini - brismu bridi

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

Theorem mapti-ckini 581

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 580	. . 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 54	. 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 34	. 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 18	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 33 ro brd 177 du sbdu 196 ckini sbckini 273 mapti sbmapti 579

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

This theorem depends on definitions: df-go 52 df-mapti 580

This theorem is referenced by: (None)