---

Step * 1 1 of Lemma permutation-s-group-sep-or


1. rv : SeparationSpace
2. sepw : x:Point ⟶ y:{y:Point| x # y}  ⟶ x # y
3. ∀a,b:Point.  SqStable(a # b)
4. x1 : Point ⟶ Point
5. x2 : Point ⟶ Point
6. [%2] : (∀x:Point. x1 (x2 x) ≡ x)
∧ (∀x:Point. x2 (x1 x) ≡ x)
∧ (∀x,y:Point.  (x1 x # x1 y ⇒ x # y))
∧ (∀x,y:Point.  (x2 x # x2 y ⇒ x # y))
7. x3 : Point ⟶ Point
8. x4 : Point ⟶ Point
9. [%3] : (∀x:Point. x3 (x4 x) ≡ x)
∧ (∀x:Point. x4 (x3 x) ≡ x)
∧ (∀x,y:Point.  (x3 x # x3 y ⇒ x # y))
∧ (∀x,y:Point.  (x4 x # x4 y ⇒ x # y))
10. y1 : Point ⟶ Point
11. y2 : Point ⟶ Point
12. [%4] : (∀x:Point. y1 (y2 x) ≡ x)
∧ (∀x:Point. y2 (y1 x) ≡ x)
∧ (∀x,y:Point.  (y1 x # y1 y ⇒ x # y))
∧ (∀x,y:Point.  (y2 x # y2 y ⇒ x # y))
13. y3 : Point ⟶ Point
14. y4 : Point ⟶ Point
15. [%5] : (∀x:Point. y3 (y4 x) ≡ x)
∧ (∀x:Point. y4 (y3 x) ≡ x)
∧ (∀x,y:Point.  (y3 x # y3 y ⇒ x # y))
∧ (∀x,y:Point.  (y4 x # y4 y ⇒ x # y))
16. a : Point
17. x1 (y1 a) # x3 (y3 a)
18. x1 (y1 a) # x1 (y3 a)
⊢ ((∃a:Point. x1 a # x3 a) ∨ (∃a:Point. x2 a # x4 a)) ∨ (∃a:Point. y1 a # y3 a) ∨ (∃a:Point. y2 a # y4 a)
BY
{ ((Sel 2 (D 0) THENA Auto) THEN (D 0 With ⌜a⌝  THENA Auto)) }

1
1. rv : SeparationSpace
2. sepw : x:Point ⟶ y:{y:Point| x # y}  ⟶ x # y
3. ∀a,b:Point.  SqStable(a # b)
4. x1 : Point ⟶ Point
5. x2 : Point ⟶ Point
6. [%2] : (∀x:Point. x1 (x2 x) ≡ x)
∧ (∀x:Point. x2 (x1 x) ≡ x)
∧ (∀x,y:Point.  (x1 x # x1 y ⇒ x # y))
∧ (∀x,y:Point.  (x2 x # x2 y ⇒ x # y))
7. x3 : Point ⟶ Point
8. x4 : Point ⟶ Point
9. [%3] : (∀x:Point. x3 (x4 x) ≡ x)
∧ (∀x:Point. x4 (x3 x) ≡ x)
∧ (∀x,y:Point.  (x3 x # x3 y ⇒ x # y))
∧ (∀x,y:Point.  (x4 x # x4 y ⇒ x # y))
10. y1 : Point ⟶ Point
11. y2 : Point ⟶ Point
12. [%4] : (∀x:Point. y1 (y2 x) ≡ x)
∧ (∀x:Point. y2 (y1 x) ≡ x)
∧ (∀x,y:Point.  (y1 x # y1 y ⇒ x # y))
∧ (∀x,y:Point.  (y2 x # y2 y ⇒ x # y))
13. y3 : Point ⟶ Point
14. y4 : Point ⟶ Point
15. [%5] : (∀x:Point. y3 (y4 x) ≡ x)
∧ (∀x:Point. y4 (y3 x) ≡ x)
∧ (∀x,y:Point.  (y3 x # y3 y ⇒ x # y))
∧ (∀x,y:Point.  (y4 x # y4 y ⇒ x # y))
16. a : Point
17. x1 (y1 a) # x3 (y3 a)
18. x1 (y1 a) # x1 (y3 a)
⊢ y1 a # y3 a

---

Latex:

---

Latex:

1.  rv  :  SeparationSpace
2.  sepw  :  x:Point  {}\mrightarrow{}  y:\{y:Point|  x  \#  y\}    {}\mrightarrow{}  x  \#  y
3.  \mforall{}a,b:Point.    SqStable(a  \#  b)
4.  x1  :  Point  {}\mrightarrow{}  Point
5.  x2  :  Point  {}\mrightarrow{}  Point
6.  [\%2]  :  (\mforall{}x:Point.  x1  (x2  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x:Point.  x2  (x1  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x,y:Point.    (x1  x  \#  x1  y  {}\mRightarrow{}  x  \#  y))
\mwedge{}  (\mforall{}x,y:Point.    (x2  x  \#  x2  y  {}\mRightarrow{}  x  \#  y))
7.  x3  :  Point  {}\mrightarrow{}  Point
8.  x4  :  Point  {}\mrightarrow{}  Point
9.  [\%3]  :  (\mforall{}x:Point.  x3  (x4  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x:Point.  x4  (x3  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x,y:Point.    (x3  x  \#  x3  y  {}\mRightarrow{}  x  \#  y))
\mwedge{}  (\mforall{}x,y:Point.    (x4  x  \#  x4  y  {}\mRightarrow{}  x  \#  y))
10.  y1  :  Point  {}\mrightarrow{}  Point
11.  y2  :  Point  {}\mrightarrow{}  Point
12.  [\%4]  :  (\mforall{}x:Point.  y1  (y2  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x:Point.  y2  (y1  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x,y:Point.    (y1  x  \#  y1  y  {}\mRightarrow{}  x  \#  y))
\mwedge{}  (\mforall{}x,y:Point.    (y2  x  \#  y2  y  {}\mRightarrow{}  x  \#  y))
13.  y3  :  Point  {}\mrightarrow{}  Point
14.  y4  :  Point  {}\mrightarrow{}  Point
15.  [\%5]  :  (\mforall{}x:Point.  y3  (y4  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x:Point.  y4  (y3  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x,y:Point.    (y3  x  \#  y3  y  {}\mRightarrow{}  x  \#  y))
\mwedge{}  (\mforall{}x,y:Point.    (y4  x  \#  y4  y  {}\mRightarrow{}  x  \#  y))
16.  a  :  Point
17.  x1  (y1  a)  \#  x3  (y3  a)
18.  x1  (y1  a)  \#  x1  (y3  a)
\mvdash{}  ((\mexists{}a:Point.  x1  a  \#  x3  a)  \mvee{}  (\mexists{}a:Point.  x2  a  \#  x4  a))
\mvee{}  (\mexists{}a:Point.  y1  a  \#  y3  a)
\mvee{}  (\mexists{}a:Point.  y2  a  \#  y4  a)


By

---

Latex:
((Sel  2  (D  0)  THENA  Auto)  THEN  (D  0  With  \mkleeneopen{}a\mkleeneclose{}    THENA  Auto))

---

Home Index