---

Step * 2 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. y2 (x2 a) # y4 (x4 a)
18. y2 (x2 a) # y2 (x4 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
{ ((OrLeft THENA Auto) THEN (OrRight 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. y2 (x2 a) # y4 (x4 a)
18. y2 (x2 a) # y2 (x4 a)
⊢ x2 a # x4 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.  y2  (x2  a)  \#  y4  (x4  a)
18.  y2  (x2  a)  \#  y2  (x4  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:
((OrLeft  THENA  Auto)  THEN  (OrRight  THENA  Auto)  THEN  (D  0  With  \mkleeneopen{}a\mkleeneclose{}    THENA  Auto))

---

Home Index