---

Step * of Lemma exists_uni_upto_char

∀T:Type. ∀r:T ⟶ T ⟶ ℙ. ∀Q:T ⟶ ℙ.  ((∃x:T. Q[x]) ⇒ (∀x,y:T.  (Q[x] ⇒ Q[y] ⇒ (x [r] y))) ⇒ (r)∃!x:T. Q[x])
BY
{ ((Unfold `exists_uni_upto` 0 
THEN GenExRepD) THENA Auto) }

1
1. T : Type@i'
2. r : T ⟶ T ⟶ ℙ@i'
3. Q : T ⟶ ℙ@i'
4. x : T@i
5. Q[x]@i
6. ∀x,y:T.  (Q[x] ⇒ Q[y] ⇒ (x [r] y))@i
⊢ ∃a:T. a r !x:T. Q[x] 

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}r:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.
    ((\mexists{}x:T.  Q[x])  {}\mRightarrow{}  (\mforall{}x,y:T.    (Q[x]  {}\mRightarrow{}  Q[y]  {}\mRightarrow{}  (x  [r]  y)))  {}\mRightarrow{}  (r)\mexists{}!x:T.  Q[x])


By

---

Latex:
((Unfold  `exists\_uni\_upto`  0 
THEN  GenExRepD)  THENA  Auto)

---

Home Index