mapti-ckini - brismu bridi

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

Theorem mapti-ckini 638

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 da is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mapti 637	. . 3 ⊢ 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
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 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
3		ax-ge-le 43	. 2 ⊢ ganai 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 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 636

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 637

This theorem is referenced by: (None)