Metamath Proof Explorer

Theorem tgaaddcpbl2

Description: The angular addition is compatible with angle congruence: by adding congruent angles together, we obtain congruent angles. Compared with tgaaddcpbl , this version handles cases where U , V and W are aligned. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses tgaaddcpbl2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgaaddcpbl2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgaaddcpbl2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgaaddcpbl2.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
tgaaddcpbl2.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgaaddcpbl2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
tgaaddcpbl2.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
tgaaddcpbl2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
tgaaddcpbl2.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
tgaaddcpbl2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
tgaaddcpbl2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tgaaddcpbl2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
tgaaddcpbl2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
tgaaddcpbl2.2 ⊢ ( 𝜑 → 𝑌 ≠ 𝑆 )
tgaaddcpbl2.3 ⊢ ( 𝜑 → 𝑉 ≠ 𝑇 )
tgaaddcpbl2.4 ⊢ ( 𝜑 → ( ( 𝑌 𝐿 𝑆 ) ∩ ( 𝑋 𝐼 𝑍 ) ) ≠ ∅ )
tgaaddcpbl2.5 ⊢ ( 𝜑 → ( ( 𝑉 𝐿 𝑇 ) ∩ ( 𝑈 𝐼 𝑊 ) ) ≠ ∅ )
tgaaddcpbl2.6 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
tgaaddcpbl2.7 ⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
Assertion tgaaddcpbl2 ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )

Proof

Step Hyp Ref Expression
1 tgaaddcpbl2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgaaddcpbl2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tgaaddcpbl2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 tgaaddcpbl2.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
5 tgaaddcpbl2.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 tgaaddcpbl2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
7 tgaaddcpbl2.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
8 tgaaddcpbl2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
9 tgaaddcpbl2.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
10 tgaaddcpbl2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11 tgaaddcpbl2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
12 tgaaddcpbl2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
13 tgaaddcpbl2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
14 tgaaddcpbl2.2 ⊢ ( 𝜑 → 𝑌 ≠ 𝑆 )
15 tgaaddcpbl2.3 ⊢ ( 𝜑 → 𝑉 ≠ 𝑇 )
16 tgaaddcpbl2.4 ⊢ ( 𝜑 → ( ( 𝑌 𝐿 𝑆 ) ∩ ( 𝑋 𝐼 𝑍 ) ) ≠ ∅ )
17 tgaaddcpbl2.5 ⊢ ( 𝜑 → ( ( 𝑉 𝐿 𝑇 ) ∩ ( 𝑈 𝐼 𝑊 ) ) ≠ ∅ )
18 tgaaddcpbl2.6 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
19 tgaaddcpbl2.7 ⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
20 4 a1i ⊢ ( 𝜑 → ∼ = ( cgrA ‘ 𝐺 ) )
21 20 eqcomd ⊢ ( 𝜑 → ( cgrA ‘ 𝐺 ) = ∼ )
22 5 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝐺 ∈ TarskiG )
23 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
24 8 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑈 ∈ 𝑃 )
25 9 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑉 ∈ 𝑃 )
26 10 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑊 ∈ 𝑃 )
27 11 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑋 ∈ 𝑃 )
28 12 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑌 ∈ 𝑃 )
29 13 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑍 ∈ 𝑃 )
30 6 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑆 ∈ 𝑃 )
31 7 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑇 ∈ 𝑃 )
32 20 19 breqdi ⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
34 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
35 20 18 breqdi ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 )
38 1 2 23 30 27 28 22 37 hlcomd ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 )
39 1 2 34 22 27 28 30 24 25 31 36 23 38 cgrahl ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑇 )
40 1 2 23 22 30 28 29 31 25 26 33 24 39 cgrahl1 ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
41 1 2 22 23 30 28 29 24 25 26 40 cgracom ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → ⟨“ 𝑈 𝑉 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑍 ”⟩ )
42 1 2 23 22 24 25 26 30 28 29 41 27 38 cgrahl1 ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → ⟨“ 𝑈 𝑉 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
43 1 2 22 23 24 25 26 27 28 29 42 cgracom ⊢ ( ( 𝜑 ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
44 43 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
45 5 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝐺 ∈ TarskiG )
46 6 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑆 ∈ 𝑃 )
47 12 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑌 ∈ 𝑃 )
48 13 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑍 ∈ 𝑃 )
49 7 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑇 ∈ 𝑃 )
50 9 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑉 ∈ 𝑃 )
51 10 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑊 ∈ 𝑃 )
52 11 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑋 ∈ 𝑃 )
53 8 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑈 ∈ 𝑃 )
54 32 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
55 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) )
56 1 34 2 45 52 47 46 55 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑌 ∈ ( 𝑆 𝐼 𝑋 ) )
57 35 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
58 1 2 34 45 52 47 46 53 50 49 57 55 cgrabtwn ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑉 ∈ ( 𝑈 𝐼 𝑇 ) )
59 1 34 2 45 53 50 49 58 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑉 ∈ ( 𝑇 𝐼 𝑈 ) )
60 1 2 23 5 11 12 6 8 9 7 35 cgrane1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
61 60 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑌 ≠ 𝑋 )
63 1 2 5 23 11 12 6 8 9 7 35 cgracom ⊢ ( 𝜑 → ⟨“ 𝑈 𝑉 𝑇 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑆 ”⟩ )
64 1 2 23 5 8 9 7 11 12 6 63 cgrane1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
65 64 necomd ⊢ ( 𝜑 → 𝑉 ≠ 𝑈 )
66 65 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → 𝑉 ≠ 𝑈 )
67 1 2 34 45 46 47 48 49 50 51 52 53 54 56 59 62 66 sacgr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
68 67 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
69 11 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑋 ∈ 𝑃 )
70 12 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑌 ∈ 𝑃 )
71 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑆 ∈ 𝑃 )
72 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝐺 ∈ TarskiG )
73 60 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑋 ≠ 𝑌 )
74 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) )
75 14 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑌 ≠ 𝑆 )
76 1 2 3 72 69 70 71 73 74 75 lnrot2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) )
77 1 2 23 69 70 71 72 69 3 76 lnhl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → ( 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑆 ) ) )
78 44 68 77 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
79 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝐺 ∈ TarskiG )
80 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑋 ∈ 𝑃 )
81 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑌 ∈ 𝑃 )
82 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑍 ∈ 𝑃 )
83 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑈 ∈ 𝑃 )
84 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑉 ∈ 𝑃 )
85 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑇 ∈ 𝑃 )
86 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑆 ∈ 𝑃 )
87 63 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → ⟨“ 𝑈 𝑉 𝑇 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑆 ”⟩ )
88 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 )
89 1 2 23 86 82 81 79 88 hlcomd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑍 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 )
90 1 2 23 79 83 84 85 80 81 86 87 82 89 cgrahl2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → ⟨“ 𝑈 𝑉 𝑇 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
91 1 2 79 23 83 84 85 80 81 82 90 cgracom ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
92 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑊 ∈ 𝑃 )
93 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
94 1 2 34 79 86 81 82 85 84 92 93 23 88 cgrahl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑇 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
95 1 2 23 85 92 84 79 94 hlcomd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → 𝑊 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑇 )
96 1 2 23 79 80 81 82 83 84 85 91 92 95 cgrahl2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
97 96 adantlr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
98 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝐺 ∈ TarskiG )
99 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑍 ∈ 𝑃 )
100 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑌 ∈ 𝑃 )
101 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑋 ∈ 𝑃 )
102 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑊 ∈ 𝑃 )
103 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑉 ∈ 𝑃 )
104 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑈 ∈ 𝑃 )
105 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑆 ∈ 𝑃 )
106 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑇 ∈ 𝑃 )
107 1 2 34 5 11 12 6 8 9 7 35 cgraswaplr ⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑋 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑈 ”⟩ )
108 107 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → ⟨“ 𝑆 𝑌 𝑋 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑈 ”⟩ )
109 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) )
110 1 34 2 98 99 100 105 109 tgbtwncom ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑌 ∈ ( 𝑆 𝐼 𝑍 ) )
111 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
112 1 2 34 98 105 100 99 106 103 102 111 110 cgrabtwn ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑉 ∈ ( 𝑇 𝐼 𝑊 ) )
113 1 2 23 5 6 12 13 7 9 10 32 cgrane2 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
114 113 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑌 ≠ 𝑍 )
115 1 2 5 23 6 12 13 7 9 10 32 cgracom ⊢ ( 𝜑 → ⟨“ 𝑇 𝑉 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑍 ”⟩ )
116 1 2 23 5 7 9 10 6 12 13 115 cgrane2 ⊢ ( 𝜑 → 𝑉 ≠ 𝑊 )
117 116 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → 𝑉 ≠ 𝑊 )
118 1 2 34 98 105 100 101 106 103 104 99 102 108 110 112 114 117 sacgr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → ⟨“ 𝑍 𝑌 𝑋 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑊 𝑉 𝑈 ”⟩ )
119 1 2 34 98 99 100 101 102 103 104 118 cgraswaplr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
120 119 adantlr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
121 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑍 ∈ 𝑃 )
122 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑌 ∈ 𝑃 )
123 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑆 ∈ 𝑃 )
124 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝐺 ∈ TarskiG )
125 113 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
126 125 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑍 ≠ 𝑌 )
127 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) )
128 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑌 ≠ 𝑆 )
129 1 2 3 124 121 122 123 126 127 128 lnrot2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑆 ∈ ( 𝑍 𝐿 𝑌 ) )
130 1 2 23 121 122 123 124 122 3 129 lnhl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ( 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∨ 𝑌 ∈ ( 𝑍 𝐼 𝑆 ) ) )
131 97 120 130 mpjaodan ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
132 eqid ⊢ ( cgrA ‘ 𝐺 ) = ( cgrA ‘ 𝐺 )
133 eleq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ↔ 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) )
134 133 adantr ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ↔ 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) )
135 eleq1 ⊢ ( 𝑏 = 𝑑 → ( 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ↔ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) )
136 135 adantl ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ↔ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) )
137 134 136 anbi12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ↔ ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ) )
138 oveq12 ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 𝐼 𝑏 ) = ( 𝑐 𝐼 𝑑 ) )
139 138 eleq2d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ) )
140 139 rexbidv ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ) )
141 eleq1 ⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ↔ 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) )
142 141 cbvrexvw ⊢ ( ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ↔ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) )
143 140 142 bitrdi ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) )
144 137 143 anbi12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) ) )
145 144 cbvopabv ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) }
146 eleq1 ⊢ ( 𝑒 = 𝑔 → ( 𝑒 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ↔ 𝑔 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) )
147 146 adantr ⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ℎ ) → ( 𝑒 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ↔ 𝑔 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) )
148 eleq1 ⊢ ( 𝑓 = ℎ → ( 𝑓 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ↔ ℎ ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) )
149 148 adantl ⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ℎ ) → ( 𝑓 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ↔ ℎ ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) )
150 147 149 anbi12d ⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ℎ ) → ( ( 𝑒 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑓 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ↔ ( 𝑔 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ ℎ ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ) )
151 oveq12 ⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ℎ ) → ( 𝑒 𝐼 𝑓 ) = ( 𝑔 𝐼 ℎ ) )
152 151 eleq2d ⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ℎ ) → ( 𝑢 ∈ ( 𝑒 𝐼 𝑓 ) ↔ 𝑢 ∈ ( 𝑔 𝐼 ℎ ) ) )
153 152 rexbidv ⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ℎ ) → ( ∃ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) 𝑢 ∈ ( 𝑒 𝐼 𝑓 ) ↔ ∃ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) 𝑢 ∈ ( 𝑔 𝐼 ℎ ) ) )
154 eleq1 ⊢ ( 𝑢 = 𝑣 → ( 𝑢 ∈ ( 𝑔 𝐼 ℎ ) ↔ 𝑣 ∈ ( 𝑔 𝐼 ℎ ) ) )
155 154 cbvrexvw ⊢ ( ∃ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) 𝑢 ∈ ( 𝑔 𝐼 ℎ ) ↔ ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑔 𝐼 ℎ ) )
156 153 155 bitrdi ⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ℎ ) → ( ∃ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) 𝑢 ∈ ( 𝑒 𝐼 𝑓 ) ↔ ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑔 𝐼 ℎ ) ) )
157 150 156 anbi12d ⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ℎ ) → ( ( ( 𝑒 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑓 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) 𝑢 ∈ ( 𝑒 𝐼 𝑓 ) ) ↔ ( ( 𝑔 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ ℎ ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑔 𝐼 ℎ ) ) ) )
158 157 cbvopabv ⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑓 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) 𝑢 ∈ ( 𝑒 𝐼 𝑓 ) ) } = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( 𝑔 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ ℎ ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑔 𝐼 ℎ ) ) }
159 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝐺 ∈ TarskiG )
160 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑆 ∈ 𝑃 )
161 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑇 ∈ 𝑃 )
162 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑈 ∈ 𝑃 )
163 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑉 ∈ 𝑃 )
164 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑊 ∈ 𝑃 )
165 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑋 ∈ 𝑃 )
166 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑌 ∈ 𝑃 )
167 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑍 ∈ 𝑃 )
168 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑌 ≠ 𝑆 )
169 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑉 ≠ 𝑇 )
170 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) )
171 165 170 eldifd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑋 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) )
172 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) )
173 167 172 eldifd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑍 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) )
174 171 173 jca ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ( 𝑋 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) )
175 inn0 ⊢ ( ( ( 𝑌 𝐿 𝑆 ) ∩ ( 𝑋 𝐼 𝑍 ) ) ≠ ∅ ↔ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑋 𝐼 𝑍 ) )
176 16 175 sylib ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑋 𝐼 𝑍 ) )
177 176 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑋 𝐼 𝑍 ) )
178 174 177 jca ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ( ( 𝑋 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑋 𝐼 𝑍 ) ) )
179 145 a1i ⊢ ( 𝜑 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) } )
180 oveq12 ⊢ ( ( 𝑐 = 𝑋 ∧ 𝑑 = 𝑍 ) → ( 𝑐 𝐼 𝑑 ) = ( 𝑋 𝐼 𝑍 ) )
181 180 eleq2d ⊢ ( ( 𝑐 = 𝑋 ∧ 𝑑 = 𝑍 ) → ( 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ↔ 𝑡 ∈ ( 𝑋 𝐼 𝑍 ) ) )
182 181 adantl ⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝑋 ∧ 𝑑 = 𝑍 ) ) → ( 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ↔ 𝑡 ∈ ( 𝑋 𝐼 𝑍 ) ) )
183 182 rexbidv ⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝑋 ∧ 𝑑 = 𝑍 ) ) → ( ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ↔ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑋 𝐼 𝑍 ) ) )
184 179 183 brab2d ⊢ ( 𝜑 → ( 𝑋 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑍 ↔ ( ( 𝑋 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
185 184 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ( 𝑋 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑍 ↔ ( ( 𝑋 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑍 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑆 ) 𝑡 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
186 178 185 mpbird ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑋 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑍 )
187 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) )
188 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝐺 ∈ TarskiG )
189 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑌 ∈ 𝑃 )
190 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑆 ∈ 𝑃 )
191 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑋 ∈ 𝑃 )
192 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑌 ≠ 𝑆 )
193 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑈 ∈ 𝑃 )
194 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 ∈ 𝑃 )
195 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑇 ∈ 𝑃 )
196 63 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → ⟨“ 𝑈 𝑉 𝑇 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑆 ”⟩ )
197 animorrl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ∨ 𝑉 = 𝑇 ) )
198 1 3 2 188 194 195 193 197 colrot2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑇 ∈ ( 𝑈 𝐿 𝑉 ) ∨ 𝑈 = 𝑉 ) )
199 1 2 34 188 193 194 195 191 189 190 196 3 198 cgracol ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
200 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑋 ≠ 𝑌 )
201 200 neneqd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → ¬ 𝑋 = 𝑌 )
202 199 201 olcnd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑆 ∈ ( 𝑋 𝐿 𝑌 ) )
203 1 2 3 188 189 190 191 192 202 200 lnrot1 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) )
204 187 203 mtand ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) )
205 204 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑇 ) )
206 162 205 eldifd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑈 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) )
207 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) )
208 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝐺 ∈ TarskiG )
209 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑌 ∈ 𝑃 )
210 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑆 ∈ 𝑃 )
211 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑍 ∈ 𝑃 )
212 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑌 ≠ 𝑆 )
213 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑇 ∈ 𝑃 )
214 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑉 ∈ 𝑃 )
215 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑊 ∈ 𝑃 )
216 115 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → ⟨“ 𝑇 𝑉 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑍 ”⟩ )
217 animorrl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ∨ 𝑉 = 𝑇 ) )
218 1 3 2 208 214 213 215 217 colcom ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑊 ∈ ( 𝑇 𝐿 𝑉 ) ∨ 𝑇 = 𝑉 ) )
219 1 2 34 208 213 214 215 210 209 211 216 3 218 cgracol ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → ( 𝑍 ∈ ( 𝑆 𝐿 𝑌 ) ∨ 𝑆 = 𝑌 ) )
220 14 necomd ⊢ ( 𝜑 → 𝑆 ≠ 𝑌 )
221 220 neneqd ⊢ ( 𝜑 → ¬ 𝑆 = 𝑌 )
222 221 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → ¬ 𝑆 = 𝑌 )
223 219 222 olcnd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑍 ∈ ( 𝑆 𝐿 𝑌 ) )
224 1 2 3 208 209 210 211 212 223 lncom ⊢ ( ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) ) → 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) )
225 207 224 mtand ⊢ ( ( 𝜑 ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ¬ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) )
226 225 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ¬ 𝑊 ∈ ( 𝑉 𝐿 𝑇 ) )
227 164 226 eldifd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑊 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) )
228 206 227 jca ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ( 𝑈 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑊 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) )
229 inn0 ⊢ ( ( ( 𝑉 𝐿 𝑇 ) ∩ ( 𝑈 𝐼 𝑊 ) ) ≠ ∅ ↔ ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑈 𝐼 𝑊 ) )
230 17 229 sylib ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑈 𝐼 𝑊 ) )
231 230 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑈 𝐼 𝑊 ) )
232 228 231 jca ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ( ( 𝑈 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑊 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑈 𝐼 𝑊 ) ) )
233 158 a1i ⊢ ( 𝜑 → { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑓 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) 𝑢 ∈ ( 𝑒 𝐼 𝑓 ) ) } = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( 𝑔 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ ℎ ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑔 𝐼 ℎ ) ) } )
234 oveq12 ⊢ ( ( 𝑔 = 𝑈 ∧ ℎ = 𝑊 ) → ( 𝑔 𝐼 ℎ ) = ( 𝑈 𝐼 𝑊 ) )
235 234 eleq2d ⊢ ( ( 𝑔 = 𝑈 ∧ ℎ = 𝑊 ) → ( 𝑣 ∈ ( 𝑔 𝐼 ℎ ) ↔ 𝑣 ∈ ( 𝑈 𝐼 𝑊 ) ) )
236 235 adantl ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝑈 ∧ ℎ = 𝑊 ) ) → ( 𝑣 ∈ ( 𝑔 𝐼 ℎ ) ↔ 𝑣 ∈ ( 𝑈 𝐼 𝑊 ) ) )
237 236 rexbidv ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝑈 ∧ ℎ = 𝑊 ) ) → ( ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑔 𝐼 ℎ ) ↔ ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑈 𝐼 𝑊 ) ) )
238 233 237 brab2d ⊢ ( 𝜑 → ( 𝑈 { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑓 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) 𝑢 ∈ ( 𝑒 𝐼 𝑓 ) ) } 𝑊 ↔ ( ( 𝑈 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑊 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑈 𝐼 𝑊 ) ) ) )
239 238 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ( 𝑈 { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑓 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) 𝑢 ∈ ( 𝑒 𝐼 𝑓 ) ) } 𝑊 ↔ ( ( 𝑈 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑊 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑣 ∈ ( 𝑉 𝐿 𝑇 ) 𝑣 ∈ ( 𝑈 𝐼 𝑊 ) ) ) )
240 232 239 mpbird ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → 𝑈 { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑓 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑢 ∈ ( 𝑉 𝐿 𝑇 ) 𝑢 ∈ ( 𝑒 𝐼 𝑓 ) ) } 𝑊 )
241 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
242 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
243 1 2 3 132 145 158 159 160 161 162 163 164 165 166 167 168 169 186 240 241 242 tgaaddcpbl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
244 exmidd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → ( 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ∨ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) )
245 131 243 244 mpjaodan ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
246 exmidd ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ∨ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ) )
247 78 245 246 mpjaodan ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
248 21 247 breqdi ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )