mapti-ckini - brismu bridi

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

Theorem mapti-ckini 709

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 708	. . 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 85	. 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 48	. 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 21	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 47 ro brd 222 du sbdu 250 ckini sbckini 347 mapti sbmapti 707

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

This theorem depends on definitions: df-go 83 df-mapti 708

This theorem is referenced by: (None)