Theorem tgaaddcpbl2 29228

Description: The angular addition is compatible with angle congruence: by adding congruent angles together, we obtain congruent angles. Compared with tgaaddcpbl 29227, 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 2768	. 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 2762	. . . . . 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 5122	. . . . . . . . . 10 ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑊”⟩)
27	26	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆((hlG‘𝐺)‘𝑌)𝑋) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑊”⟩)
28		eqid 2762	. . . . . . . . . 10 ⊢ (dist‘𝐺) = (dist‘𝐺)
29		tgaaddcpbl2.6	. . . . . . . . . . . 12 ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)
30	2, 29	breqdi 5122	. . . . . . . . . . 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 28945	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑆((hlG‘𝐺)‘𝑌)𝑋) → 𝑋((hlG‘𝐺)‘𝑌)𝑆)
34	4, 5, 28, 7, 16, 18, 22, 10, 12, 24, 31, 8, 33	cgrahl 29210	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆((hlG‘𝐺)‘𝑌)𝑋) → 𝑈((hlG‘𝐺)‘𝑉)𝑇)
35	4, 5, 8, 7, 22, 18, 20, 24, 12, 14, 27, 10, 34	cgrahl1 29198	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆((hlG‘𝐺)‘𝑌)𝑋) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑊”⟩)
36	4, 5, 7, 8, 22, 18, 20, 10, 12, 14, 35	cgracom 29204	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆((hlG‘𝐺)‘𝑌)𝑋) → ⟨“𝑈𝑉𝑊”⟩(cgrA‘𝐺)⟨“𝑆𝑌𝑍”⟩)
37	4, 5, 8, 7, 10, 12, 14, 22, 18, 20, 36, 16, 33	cgrahl1 29198	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆((hlG‘𝐺)‘𝑌)𝑋) → ⟨“𝑈𝑉𝑊”⟩(cgrA‘𝐺)⟨“𝑋𝑌𝑍”⟩)
38	4, 5, 7, 8, 10, 12, 14, 16, 18, 20, 37	cgracom 29204	. . . . 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 28826	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑆)) → 𝑌 ∈ (𝑆𝐼𝑋))
52	30	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑆)) → ⟨“𝑋𝑌𝑆”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑇”⟩)
53	4, 5, 28, 40, 47, 42, 41, 48, 45, 44, 52, 50	cgrabtwn 29209	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑆)) → 𝑉 ∈ (𝑈𝐼𝑇))
54	4, 28, 5, 40, 48, 45, 44, 53	tgbtwncom 28826	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑆)) → 𝑉 ∈ (𝑇𝐼𝑈))
55	4, 5, 8, 6, 15, 17, 21, 9, 11, 23, 30	cgrane1 29194	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
56	55	necomd 3012	. . . . . . 7 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
57	56	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑆)) → 𝑌 ≠ 𝑋)
58	4, 5, 6, 8, 15, 17, 21, 9, 11, 23, 30	cgracom 29204	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑈𝑉𝑇”⟩(cgrA‘𝐺)⟨“𝑋𝑌𝑆”⟩)
59	4, 5, 8, 6, 9, 11, 23, 15, 17, 21, 58	cgrane1 29194	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
60	59	necomd 3012	. . . . . . 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 29214	. . . . 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 28967	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐿𝑆)) → 𝑆 ∈ (𝑋𝐿𝑌))
74	4, 5, 8, 64, 65, 66, 67, 64, 68, 73	lnhl 28956	. . . 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 28945	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑆((hlG‘𝐺)‘𝑌)𝑍) → 𝑍((hlG‘𝐺)‘𝑌)𝑆)
87	4, 5, 8, 76, 80, 81, 82, 77, 78, 83, 84, 79, 86	cgrahl2 29199	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑆((hlG‘𝐺)‘𝑌)𝑍) → ⟨“𝑈𝑉𝑇”⟩(cgrA‘𝐺)⟨“𝑋𝑌𝑍”⟩)
88	4, 5, 76, 8, 80, 81, 82, 77, 78, 79, 87	cgracom 29204	. . . . . . 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 29210	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑆((hlG‘𝐺)‘𝑌)𝑍) → 𝑇((hlG‘𝐺)‘𝑉)𝑊)
92	4, 5, 8, 82, 89, 81, 76, 91	hlcomd 28945	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑆((hlG‘𝐺)‘𝑌)𝑍) → 𝑊((hlG‘𝐺)‘𝑉)𝑇)
93	4, 5, 8, 76, 77, 78, 79, 80, 81, 82, 88, 89, 92	cgrahl2 29199	. . . . . 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 29208	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑆𝑌𝑋”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑈”⟩)
105	104	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑌 ∈ (𝑍𝐼𝑆)) → ⟨“𝑆𝑌𝑋”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑈”⟩)
106		simpr 490	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑌 ∈ (𝑍𝐼𝑆)) → 𝑌 ∈ (𝑍𝐼𝑆))
107	4, 28, 5, 95, 96, 97, 102, 106	tgbtwncom 28826	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑌 ∈ (𝑍𝐼𝑆)) → 𝑌 ∈ (𝑆𝐼𝑍))
108	26	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑌 ∈ (𝑍𝐼𝑆)) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑊”⟩)
109	4, 5, 28, 95, 102, 97, 96, 103, 100, 99, 108, 107	cgrabtwn 29209	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑌 ∈ (𝑍𝐼𝑆)) → 𝑉 ∈ (𝑇𝐼𝑊))
110	4, 5, 8, 6, 21, 17, 19, 23, 11, 13, 26	cgrane2 29195	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ≠ 𝑍)
111	110	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑌 ∈ (𝑍𝐼𝑆)) → 𝑌 ≠ 𝑍)
112	4, 5, 6, 8, 21, 17, 19, 23, 11, 13, 26	cgracom 29204	. . . . . . . . . 10 ⊢ (𝜑 → ⟨“𝑇𝑉𝑊”⟩(cgrA‘𝐺)⟨“𝑆𝑌𝑍”⟩)
113	4, 5, 8, 6, 23, 11, 13, 21, 17, 19, 112	cgrane2 29195	. . . . . . . . 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 29214	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑌 ∈ (𝑍𝐼𝑆)) → ⟨“𝑍𝑌𝑋”⟩(cgrA‘𝐺)⟨“𝑊𝑉𝑈”⟩)
116	4, 5, 28, 95, 96, 97, 98, 99, 100, 101, 115	cgraswaplr 29208	. . . . . 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 3012	. . . . . . . 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 28967	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑍 ∈ (𝑌𝐿𝑆)) → 𝑆 ∈ (𝑍𝐿𝑌))
127	4, 5, 8, 118, 119, 120, 121, 119, 68, 126	lnhl 28956	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑍 ∈ (𝑌𝐿𝑆)) → (𝑆((hlG‘𝐺)‘𝑌)𝑍 ∨ 𝑌 ∈ (𝑍𝐼𝑆)))
128	94, 117, 127	mpjaodan 973	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑍 ∈ (𝑌𝐿𝑆)) → ⟨“𝑋𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑊”⟩)
129		eqid 2762	. . . . 5 ⊢ (cgrA‘𝐺) = (cgrA‘𝐺)
130		eleq1 2850	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ↔ 𝑐 ∈ (𝑃 ∖ (𝑌𝐿𝑆))))
131	130	adantr 486	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ↔ 𝑐 ∈ (𝑃 ∖ (𝑌𝐿𝑆))))
132		eleq1 2850	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ↔ 𝑑 ∈ (𝑃 ∖ (𝑌𝐿𝑆))))
133	132	adantl 487	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ↔ 𝑑 ∈ (𝑃 ∖ (𝑌𝐿𝑆))))
134	131, 133	anbi12d 644	. . . . . . 7 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ↔ (𝑐 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑌𝐿𝑆)))))
135		oveq12 7425	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎𝐼𝑏) = (𝑐𝐼𝑑))
136	135	eleq2d 2848	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑠 ∈ (𝑎𝐼𝑏) ↔ 𝑠 ∈ (𝑐𝐼𝑑)))
137	136	rexbidv 3188	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏) ↔ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑐𝐼𝑑)))
138		eleq1 2850	. . . . . . . . 9 ⊢ (𝑠 = 𝑡 → (𝑠 ∈ (𝑐𝐼𝑑) ↔ 𝑡 ∈ (𝑐𝐼𝑑)))
139	138	cbvrexvw 3243	. . . . . . . 8 ⊢ (∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑐𝐼𝑑) ↔ ∃𝑡 ∈ (𝑌𝐿𝑆)𝑡 ∈ (𝑐𝐼𝑑))
140	137, 139	bitrdi 290	. . . . . . 7 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏) ↔ ∃𝑡 ∈ (𝑌𝐿𝑆)𝑡 ∈ (𝑐𝐼𝑑)))
141	134, 140	anbi12d 644	. . . . . 6 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏)) ↔ ((𝑐 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑡 ∈ (𝑌𝐿𝑆)𝑡 ∈ (𝑐𝐼𝑑))))
142	141	cbvopabv 5182	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))} = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑡 ∈ (𝑌𝐿𝑆)𝑡 ∈ (𝑐𝐼𝑑))}
143		eleq1 2850	. . . . . . . . 9 ⊢ (𝑒 = 𝑔 → (𝑒 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ↔ 𝑔 ∈ (𝑃 ∖ (𝑉𝐿𝑇))))
144	143	adantr 486	. . . . . . . 8 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = ℎ) → (𝑒 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ↔ 𝑔 ∈ (𝑃 ∖ (𝑉𝐿𝑇))))
145		eleq1 2850	. . . . . . . . 9 ⊢ (𝑓 = ℎ → (𝑓 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ↔ ℎ ∈ (𝑃 ∖ (𝑉𝐿𝑇))))
146	145	adantl 487	. . . . . . . 8 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = ℎ) → (𝑓 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ↔ ℎ ∈ (𝑃 ∖ (𝑉𝐿𝑇))))
147	144, 146	anbi12d 644	. . . . . . 7 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = ℎ) → ((𝑒 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑓 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ↔ (𝑔 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ ℎ ∈ (𝑃 ∖ (𝑉𝐿𝑇)))))
148		oveq12 7425	. . . . . . . . . 10 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = ℎ) → (𝑒𝐼𝑓) = (𝑔𝐼ℎ))
149	148	eleq2d 2848	. . . . . . . . 9 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = ℎ) → (𝑢 ∈ (𝑒𝐼𝑓) ↔ 𝑢 ∈ (𝑔𝐼ℎ)))
150	149	rexbidv 3188	. . . . . . . 8 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = ℎ) → (∃𝑢 ∈ (𝑉𝐿𝑇)𝑢 ∈ (𝑒𝐼𝑓) ↔ ∃𝑢 ∈ (𝑉𝐿𝑇)𝑢 ∈ (𝑔𝐼ℎ)))
151		eleq1 2850	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → (𝑢 ∈ (𝑔𝐼ℎ) ↔ 𝑣 ∈ (𝑔𝐼ℎ)))
152	151	cbvrexvw 3243	. . . . . . . 8 ⊢ (∃𝑢 ∈ (𝑉𝐿𝑇)𝑢 ∈ (𝑔𝐼ℎ) ↔ ∃𝑣 ∈ (𝑉𝐿𝑇)𝑣 ∈ (𝑔𝐼ℎ))
153	150, 152	bitrdi 290	. . . . . . 7 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = ℎ) → (∃𝑢 ∈ (𝑉𝐿𝑇)𝑢 ∈ (𝑒𝐼𝑓) ↔ ∃𝑣 ∈ (𝑉𝐿𝑇)𝑣 ∈ (𝑔𝐼ℎ)))
154	147, 153	anbi12d 644	. . . . . 6 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = ℎ) → (((𝑒 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑓 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑢 ∈ (𝑉𝐿𝑇)𝑢 ∈ (𝑒𝐼𝑓)) ↔ ((𝑔 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ ℎ ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑣 ∈ (𝑉𝐿𝑇)𝑣 ∈ (𝑔𝐼ℎ))))
155	154	cbvopabv 5182	. . . . 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 3913	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → 𝑋 ∈ (𝑃 ∖ (𝑌𝐿𝑆)))
170		simpr 490	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → ¬ 𝑍 ∈ (𝑌𝐿𝑆))
171	164, 170	eldifd 3913	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → 𝑍 ∈ (𝑃 ∖ (𝑌𝐿𝑆)))
172	169, 171	jca 521	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → (𝑋 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑍 ∈ (𝑃 ∖ (𝑌𝐿𝑆))))
173		tgaaddcpbl2.4	. . . . . . . . 9 ⊢ (𝜑 → ((𝑌𝐿𝑆) ∩ (𝑋𝐼𝑍)) ≠ ∅)
174		inn0 4323	. . . . . . . . 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 7425	. . . . . . . . . . 11 ⊢ ((𝑐 = 𝑋 ∧ 𝑑 = 𝑍) → (𝑐𝐼𝑑) = (𝑋𝐼𝑍))
180	179	eleq2d 2848	. . . . . . . . . 10 ⊢ ((𝑐 = 𝑋 ∧ 𝑑 = 𝑍) → (𝑡 ∈ (𝑐𝐼𝑑) ↔ 𝑡 ∈ (𝑋𝐼𝑍)))
181	180	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 = 𝑋 ∧ 𝑑 = 𝑍)) → (𝑡 ∈ (𝑐𝐼𝑑) ↔ 𝑡 ∈ (𝑋𝐼𝑍)))
182	181	rexbidv 3188	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 = 𝑋 ∧ 𝑑 = 𝑍)) → (∃𝑡 ∈ (𝑌𝐿𝑆)𝑡 ∈ (𝑐𝐼𝑑) ↔ ∃𝑡 ∈ (𝑌𝐿𝑆)𝑡 ∈ (𝑋𝐼𝑍)))
183	178, 182	brab2d 5520	. . . . . . 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 28898	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑈 ∈ (𝑉𝐿𝑇)) → (𝑇 ∈ (𝑈𝐿𝑉) ∨ 𝑈 = 𝑉))
198	4, 5, 28, 187, 192, 193, 194, 190, 188, 189, 195, 68, 197	cgracol 29211	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑈 ∈ (𝑉𝐿𝑇)) → (𝑆 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))
199	55	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑈 ∈ (𝑉𝐿𝑇)) → 𝑋 ≠ 𝑌)
200	199	neneqd 2962	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑈 ∈ (𝑉𝐿𝑇)) → ¬ 𝑋 = 𝑌)
201	198, 200	olcnd 891	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑈 ∈ (𝑉𝐿𝑇)) → 𝑆 ∈ (𝑋𝐿𝑌))
202	4, 5, 68, 187, 188, 189, 190, 191, 201, 199	lnrot1 28966	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ 𝑈 ∈ (𝑉𝐿𝑇)) → 𝑋 ∈ (𝑌𝐿𝑆))
203	186, 202	mtand 828	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) → ¬ 𝑈 ∈ (𝑉𝐿𝑇))
204	203	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → ¬ 𝑈 ∈ (𝑉𝐿𝑇))
205	159, 204	eldifd 3913	. . . . . . . 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 28896	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) ∧ 𝑊 ∈ (𝑉𝐿𝑇)) → (𝑊 ∈ (𝑇𝐿𝑉) ∨ 𝑇 = 𝑉))
218	4, 5, 28, 207, 212, 213, 214, 209, 208, 210, 215, 68, 217	cgracol 29211	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) ∧ 𝑊 ∈ (𝑉𝐿𝑇)) → (𝑍 ∈ (𝑆𝐿𝑌) ∨ 𝑆 = 𝑌))
219	71	necomd 3012	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ≠ 𝑌)
220	219	neneqd 2962	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ 𝑆 = 𝑌)
221	220	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) ∧ 𝑊 ∈ (𝑉𝐿𝑇)) → ¬ 𝑆 = 𝑌)
222	218, 221	olcnd 891	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) ∧ 𝑊 ∈ (𝑉𝐿𝑇)) → 𝑍 ∈ (𝑆𝐿𝑌))
223	4, 5, 68, 207, 208, 209, 210, 211, 222	lncom 28965	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) ∧ 𝑊 ∈ (𝑉𝐿𝑇)) → 𝑍 ∈ (𝑌𝐿𝑆))
224	206, 223	mtand 828	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → ¬ 𝑊 ∈ (𝑉𝐿𝑇))
225	224	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → ¬ 𝑊 ∈ (𝑉𝐿𝑇))
226	161, 225	eldifd 3913	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → 𝑊 ∈ (𝑃 ∖ (𝑉𝐿𝑇)))
227	205, 226	jca 521	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → (𝑈 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑊 ∈ (𝑃 ∖ (𝑉𝐿𝑇))))
228		tgaaddcpbl2.5	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉𝐿𝑇) ∩ (𝑈𝐼𝑊)) ≠ ∅)
229		inn0 4323	. . . . . . . . 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 7425	. . . . . . . . . . 11 ⊢ ((𝑔 = 𝑈 ∧ ℎ = 𝑊) → (𝑔𝐼ℎ) = (𝑈𝐼𝑊))
235	234	eleq2d 2848	. . . . . . . . . 10 ⊢ ((𝑔 = 𝑈 ∧ ℎ = 𝑊) → (𝑣 ∈ (𝑔𝐼ℎ) ↔ 𝑣 ∈ (𝑈𝐼𝑊)))
236	235	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 = 𝑈 ∧ ℎ = 𝑊)) → (𝑣 ∈ (𝑔𝐼ℎ) ↔ 𝑣 ∈ (𝑈𝐼𝑊)))
237	236	rexbidv 3188	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 = 𝑈 ∧ ℎ = 𝑊)) → (∃𝑣 ∈ (𝑉𝐿𝑇)𝑣 ∈ (𝑔𝐼ℎ) ↔ ∃𝑣 ∈ (𝑉𝐿𝑇)𝑣 ∈ (𝑈𝐼𝑊)))
238	233, 237	brab2d 5520	. . . . . . 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 29227	. . . 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 5122	1 ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∃wrex 3088   ∖ cdif 3899   ∩ cin 3901  ∅c0 4282   class class class wbr 5107  {copab 5171  ‘cfv 6537  (class class class)co 7416  ⟨“cs3 14913  Basecbs 17303  distcds 17353  TarskiGcstrkg 28764  Itvcitv 28770  LineGclng 28771  hlGchlg 28938  cgrAccgra 29189

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-cnex 11181  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201  ax-pre-mulgt0 11202

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-oadd 8462  df-er 8699  df-map 8831  df-pm 8832  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-dju 9909  df-card 9947  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274  df-sub 11468  df-neg 11469  df-nn 12259  df-2 12328  df-3 12329  df-n0 12530  df-xnn0 12603  df-z 12617  df-uz 12889  df-fz 13562  df-fzo 13710  df-hash 14395  df-word 14579  df-concat 14636  df-s1 14663  df-s2 14919  df-s3 14920  df-trkgc 28785  df-trkgb 28786  df-trkgcb 28787  df-trkgld 28789  df-trkg 28790  df-cgrg 28849  df-leg 28921  df-hlg 28939  df-mir 29000  df-rag 29044  df-perpg 29046  df-hpg 29111  df-mid 29154  df-lmi 29155  df-cgra 29190

This theorem is used by:  angmndaddcpbl  29261