brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  k-ceihi

---

Theorem k-ceihi 234

Description: {cei'i} is the terminal object. (Contributed by la korvo, 4-Jan-2025.)

Assertion

Ref	Expression
k-ceihi	⊢ ganai broda gi cei'i

---

Proof of Theorem k-ceihi

Step	Hyp	Ref	Expression
1		ceihi 232	. 2 ⊢ cei'i
2	1	ki 12	1 ⊢ ganai broda gi cei'i

Colors of variables: sumti selbri bridi

Syntax hints:  cei'i bceihi 230

This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 15  ax-ge-le 43  ax-ge-re 44  ax-ge-in 45  ax-gen2 195  ax-qi2 204

This theorem depends on definitions:  df-go 61  df-o 167  df-du 215  df-ceihi 231

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator