---

Step * of Lemma sp-meet-is-top

∀[x,y:Sierpinski].  (x ∧ y = ⊤ ∈ Sierpinski ⇐⇒ (x = ⊤ ∈ Sierpinski) ∧ (y = ⊤ ∈ Sierpinski))
BY
{ TACTIC:(InstLemma `Sierpinski-unequal-1` [] THEN Auto THEN Thin 2 THEN D 2 THEN D -2) }

1
1. (⊥ = ⊤ ∈ (ℕ ⟶ 𝔹)) ⇒ False
2. x : Base
3. x1 : Base
4. x = x1 ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
5. x ∈ ℕ ⟶ 𝔹
6. x1 ∈ ℕ ⟶ 𝔹
7. x = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ x1 = ⊥ ∈ (ℕ ⟶ 𝔹)
8. y : Base
9. y1 : Base
10. y = y1 ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
11. y ∈ ℕ ⟶ 𝔹
12. y1 ∈ ℕ ⟶ 𝔹
13. y = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ y1 = ⊥ ∈ (ℕ ⟶ 𝔹)
14. x ∧ y = ⊤ ∈ Sierpinski
⊢ x = ⊤ ∈ Sierpinski

2
1. (⊥ = ⊤ ∈ (ℕ ⟶ 𝔹)) ⇒ False
2. x : Base
3. x1 : Base
4. x = x1 ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
5. x ∈ ℕ ⟶ 𝔹
6. x1 ∈ ℕ ⟶ 𝔹
7. x = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ x1 = ⊥ ∈ (ℕ ⟶ 𝔹)
8. y : Base
9. y1 : Base
10. y = y1 ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
11. y ∈ ℕ ⟶ 𝔹
12. y1 ∈ ℕ ⟶ 𝔹
13. y = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ y1 = ⊥ ∈ (ℕ ⟶ 𝔹)
14. x ∧ y = ⊤ ∈ Sierpinski
⊢ y = ⊤ ∈ Sierpinski

3
1. (⊥ = ⊤ ∈ (ℕ ⟶ 𝔹)) ⇒ False
2. x : Base
3. x1 : Base
4. x = x1 ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
5. x ∈ ℕ ⟶ 𝔹
6. x1 ∈ ℕ ⟶ 𝔹
7. x = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ x1 = ⊥ ∈ (ℕ ⟶ 𝔹)
8. y : Sierpinski
9. x = ⊤ ∈ Sierpinski
10. y = ⊤ ∈ Sierpinski
⊢ x ∧ y = ⊤ ∈ Sierpinski

---

Latex:

---

Latex:
\mforall{}[x,y:Sierpinski].    (x  \mwedge{}  y  =  \mtop{}  \mLeftarrow{}{}\mRightarrow{}  (x  =  \mtop{})  \mwedge{}  (y  =  \mtop{}))


By

---

Latex:
TACTIC:(InstLemma  `Sierpinski-unequal-1`  []  THEN  Auto  THEN  Thin  2  THEN  D  2  THEN  D  -2)

---

Home Index