Theorem tgaaddcpbl2 29353

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

Hypotheses

Ref	Expression
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

Ref	Expression
tgaaddcpbl2	⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)

Proof of Theorem tgaaddcpbl2

Dummy variables 𝑡 𝑣 𝑐 𝑑 𝑔 ℎ 𝑎 𝑏 𝑠 𝑒 𝑓 𝑢 are mutually distinct and distinct from all other variables.

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∃wrex 3086   ∖ cdif 4045   ∩ cin 4089  ∅c0 4278   class class class wbr 5102  {copab 5166  ‘cfv 6538  (class class class)co 7420  ⟨“cs3 14993  Basecbs 17387  distcds 17437  TarskiGcstrkg 28889  Itvcitv 28895  LineGclng 28896  hlGchlg 29063  cgrAccgra 29314

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-oadd 8480  df-er 8717  df-map 8849  df-pm 8850  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-dju 9982  df-card 10020  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-2 12405  df-3 12406  df-n0 12607  df-xnn0 12680  df-z 12694  df-uz 12966  df-fz 13640  df-fzo 13789  df-hash 14475  df-word 14659  df-concat 14716  df-s1 14743  df-s2 14999  df-s3 15000  df-trkgc 28910  df-trkgb 28911  df-trkgcb 28912  df-trkgld 28914  df-trkg 28915  df-cgrg 28974  df-leg 29046  df-hlg 29064  df-mir 29125  df-rag 29169  df-perpg 29171  df-hpg 29236  df-mid 29279  df-lmi 29280  df-cgra 29315

This theorem is used by:  angmgmaddcpbl  29390