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	$⊢ P = {Base}_{G}$
	tgaaddcpbl2.i	$⊢ I = Itv (G)$
	tgaaddcpbl2.l	$⊢ L = {Line}_{𝒢} (G)$
	tgaaddcpbl2.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	tgaaddcpbl2.1	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgaaddcpbl2.s	$⊢ φ \to S \in P$
	tgaaddcpbl2.t	$⊢ φ \to T \in P$
	tgaaddcpbl2.u	$⊢ φ \to U \in P$
	tgaaddcpbl2.v	$⊢ φ \to V \in P$
	tgaaddcpbl2.w	$⊢ φ \to W \in P$
	tgaaddcpbl2.x	$⊢ φ \to X \in P$
	tgaaddcpbl2.y	$⊢ φ \to Y \in P$
	tgaaddcpbl2.z	$⊢ φ \to Z \in P$
	tgaaddcpbl2.2	$⊢ φ \to Y \neq S$
	tgaaddcpbl2.3	$⊢ φ \to V \neq T$
	tgaaddcpbl2.4	$⊢ φ \to (Y L S) \cap (X I Z) \neq \emptyset$
	tgaaddcpbl2.5	$⊢ φ \to (V L T) \cap (U I W) \neq \emptyset$
	tgaaddcpbl2.6	$⊢ φ \to ⟨“ X Y S ”⟩ \underset{˙}{\sim} ⟨“ U V T ”⟩$
	tgaaddcpbl2.7	$⊢ φ \to ⟨“ S Y Z ”⟩ \underset{˙}{\sim} ⟨“ T V W ”⟩$
Assertion	tgaaddcpbl2	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$

Proof

Step	Hyp	Ref	Expression
1		tgaaddcpbl2.p	$⊢ P = {Base}_{G}$
2		tgaaddcpbl2.i	$⊢ I = Itv (G)$
3		tgaaddcpbl2.l	$⊢ L = {Line}_{𝒢} (G)$
4		tgaaddcpbl2.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
5		tgaaddcpbl2.1	$⊢ φ \to G \in 𝒢_{Tarski}$
6		tgaaddcpbl2.s	$⊢ φ \to S \in P$
7		tgaaddcpbl2.t	$⊢ φ \to T \in P$
8		tgaaddcpbl2.u	$⊢ φ \to U \in P$
9		tgaaddcpbl2.v	$⊢ φ \to V \in P$
10		tgaaddcpbl2.w	$⊢ φ \to W \in P$
11		tgaaddcpbl2.x	$⊢ φ \to X \in P$
12		tgaaddcpbl2.y	$⊢ φ \to Y \in P$
13		tgaaddcpbl2.z	$⊢ φ \to Z \in P$
14		tgaaddcpbl2.2	$⊢ φ \to Y \neq S$
15		tgaaddcpbl2.3	$⊢ φ \to V \neq T$
16		tgaaddcpbl2.4	$⊢ φ \to (Y L S) \cap (X I Z) \neq \emptyset$
17		tgaaddcpbl2.5	$⊢ φ \to (V L T) \cap (U I W) \neq \emptyset$
18		tgaaddcpbl2.6	$⊢ φ \to ⟨“ X Y S ”⟩ \underset{˙}{\sim} ⟨“ U V T ”⟩$
19		tgaaddcpbl2.7	$⊢ φ \to ⟨“ S Y Z ”⟩ \underset{˙}{\sim} ⟨“ T V W ”⟩$
20	4	a1i	$⊢ φ \to \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
21	20	eqcomd	$⊢ φ \to \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
22	5	adantr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to G \in 𝒢_{Tarski}$
23		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
24	8	adantr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to U \in P$
25	9	adantr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to V \in P$
26	10	adantr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to W \in P$
27	11	adantr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to X \in P$
28	12	adantr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to Y \in P$
29	13	adantr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to Z \in P$
30	6	adantr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to S \in P$
31	7	adantr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to T \in P$
32	20 19	breqdi	$⊢ φ \to ⟨“ S Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ T V W ”⟩$
33	32	adantr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to ⟨“ S Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ T V W ”⟩$
34		eqid	$⊢ dist (G) = dist (G)$
35	20 18	breqdi	$⊢ φ \to ⟨“ X Y S ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V T ”⟩$
36	35	adantr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to ⟨“ X Y S ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V T ”⟩$
37		simpr	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to S {hl}_{𝒢} (G) (Y) X$
38	1 2 23 30 27 28 22 37	hlcomd	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to X {hl}_{𝒢} (G) (Y) S$
39	1 2 34 22 27 28 30 24 25 31 36 23 38	cgrahl	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to U {hl}_{𝒢} (G) (V) T$
40	1 2 23 22 30 28 29 31 25 26 33 24 39	cgrahl1	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to ⟨“ S Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
41	1 2 22 23 30 28 29 24 25 26 40	cgracom	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to ⟨“ U V W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ S Y Z ”⟩$
42	1 2 23 22 24 25 26 30 28 29 41 27 38	cgrahl1	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to ⟨“ U V W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
43	1 2 22 23 24 25 26 27 28 29 42	cgracom	$⊢ (φ \land S {hl}_{𝒢} (G) (Y) X) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
44	43	adantlr	$⊢ ((φ \land X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) X) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
45	5	adantr	$⊢ (φ \land Y \in (X I S)) \to G \in 𝒢_{Tarski}$
46	6	adantr	$⊢ (φ \land Y \in (X I S)) \to S \in P$
47	12	adantr	$⊢ (φ \land Y \in (X I S)) \to Y \in P$
48	13	adantr	$⊢ (φ \land Y \in (X I S)) \to Z \in P$
49	7	adantr	$⊢ (φ \land Y \in (X I S)) \to T \in P$
50	9	adantr	$⊢ (φ \land Y \in (X I S)) \to V \in P$
51	10	adantr	$⊢ (φ \land Y \in (X I S)) \to W \in P$
52	11	adantr	$⊢ (φ \land Y \in (X I S)) \to X \in P$
53	8	adantr	$⊢ (φ \land Y \in (X I S)) \to U \in P$
54	32	adantr	$⊢ (φ \land Y \in (X I S)) \to ⟨“ S Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ T V W ”⟩$
55		simpr	$⊢ (φ \land Y \in (X I S)) \to Y \in (X I S)$
56	1 34 2 45 52 47 46 55	tgbtwncom	$⊢ (φ \land Y \in (X I S)) \to Y \in (S I X)$
57	35	adantr	$⊢ (φ \land Y \in (X I S)) \to ⟨“ X Y S ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V T ”⟩$
58	1 2 34 45 52 47 46 53 50 49 57 55	cgrabtwn	$⊢ (φ \land Y \in (X I S)) \to V \in (U I T)$
59	1 34 2 45 53 50 49 58	tgbtwncom	$⊢ (φ \land Y \in (X I S)) \to V \in (T I U)$
60	1 2 23 5 11 12 6 8 9 7 35	cgrane1	$⊢ φ \to X \neq Y$
61	60	necomd	$⊢ φ \to Y \neq X$
62	61	adantr	$⊢ (φ \land Y \in (X I S)) \to Y \neq X$
63	1 2 5 23 11 12 6 8 9 7 35	cgracom	$⊢ φ \to ⟨“ U V T ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y S ”⟩$
64	1 2 23 5 8 9 7 11 12 6 63	cgrane1	$⊢ φ \to U \neq V$
65	64	necomd	$⊢ φ \to V \neq U$
66	65	adantr	$⊢ (φ \land Y \in (X I S)) \to V \neq U$
67	1 2 34 45 46 47 48 49 50 51 52 53 54 56 59 62 66	sacgr	$⊢ (φ \land Y \in (X I S)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
68	67	adantlr	$⊢ ((φ \land X \in (Y L S)) \land Y \in (X I S)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
69	11	adantr	$⊢ (φ \land X \in (Y L S)) \to X \in P$
70	12	adantr	$⊢ (φ \land X \in (Y L S)) \to Y \in P$
71	6	adantr	$⊢ (φ \land X \in (Y L S)) \to S \in P$
72	5	adantr	$⊢ (φ \land X \in (Y L S)) \to G \in 𝒢_{Tarski}$
73	60	adantr	$⊢ (φ \land X \in (Y L S)) \to X \neq Y$
74		simpr	$⊢ (φ \land X \in (Y L S)) \to X \in (Y L S)$
75	14	adantr	$⊢ (φ \land X \in (Y L S)) \to Y \neq S$
76	1 2 3 72 69 70 71 73 74 75	lnrot2	$⊢ (φ \land X \in (Y L S)) \to S \in (X L Y)$
77	1 2 23 69 70 71 72 69 3 76	lnhl	$⊢ (φ \land X \in (Y L S)) \to (S {hl}_{𝒢} (G) (Y) X \lor Y \in (X I S))$
78	44 68 77	mpjaodan	$⊢ (φ \land X \in (Y L S)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
79	5	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to G \in 𝒢_{Tarski}$
80	11	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to X \in P$
81	12	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to Y \in P$
82	13	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to Z \in P$
83	8	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to U \in P$
84	9	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to V \in P$
85	7	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to T \in P$
86	6	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to S \in P$
87	63	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to ⟨“ U V T ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y S ”⟩$
88		simpr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to S {hl}_{𝒢} (G) (Y) Z$
89	1 2 23 86 82 81 79 88	hlcomd	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to Z {hl}_{𝒢} (G) (Y) S$
90	1 2 23 79 83 84 85 80 81 86 87 82 89	cgrahl2	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to ⟨“ U V T ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
91	1 2 79 23 83 84 85 80 81 82 90	cgracom	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V T ”⟩$
92	10	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to W \in P$
93	32	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to ⟨“ S Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ T V W ”⟩$
94	1 2 34 79 86 81 82 85 84 92 93 23 88	cgrahl	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to T {hl}_{𝒢} (G) (V) W$
95	1 2 23 85 92 84 79 94	hlcomd	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to W {hl}_{𝒢} (G) (V) T$
96	1 2 23 79 80 81 82 83 84 85 91 92 95	cgrahl2	$⊢ ((φ \land \neg X \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
97	96	adantlr	$⊢ (((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \land S {hl}_{𝒢} (G) (Y) Z) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
98	5	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to G \in 𝒢_{Tarski}$
99	13	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to Z \in P$
100	12	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to Y \in P$
101	11	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to X \in P$
102	10	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to W \in P$
103	9	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to V \in P$
104	8	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to U \in P$
105	6	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to S \in P$
106	7	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to T \in P$
107	1 2 34 5 11 12 6 8 9 7 35	cgraswaplr	$⊢ φ \to ⟨“ S Y X ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ T V U ”⟩$
108	107	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to ⟨“ S Y X ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ T V U ”⟩$
109		simpr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to Y \in (Z I S)$
110	1 34 2 98 99 100 105 109	tgbtwncom	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to Y \in (S I Z)$
111	32	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to ⟨“ S Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ T V W ”⟩$
112	1 2 34 98 105 100 99 106 103 102 111 110	cgrabtwn	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to V \in (T I W)$
113	1 2 23 5 6 12 13 7 9 10 32	cgrane2	$⊢ φ \to Y \neq Z$
114	113	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to Y \neq Z$
115	1 2 5 23 6 12 13 7 9 10 32	cgracom	$⊢ φ \to ⟨“ T V W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ S Y Z ”⟩$
116	1 2 23 5 7 9 10 6 12 13 115	cgrane2	$⊢ φ \to V \neq W$
117	116	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to V \neq W$
118	1 2 34 98 105 100 101 106 103 104 99 102 108 110 112 114 117	sacgr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to ⟨“ Z Y X ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ W V U ”⟩$
119	1 2 34 98 99 100 101 102 103 104 118	cgraswaplr	$⊢ ((φ \land \neg X \in (Y L S)) \land Y \in (Z I S)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
120	119	adantlr	$⊢ (((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \land Y \in (Z I S)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
121	13	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \to Z \in P$
122	12	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \to Y \in P$
123	6	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \to S \in P$
124	5	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \to G \in 𝒢_{Tarski}$
125	113	necomd	$⊢ φ \to Z \neq Y$
126	125	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \to Z \neq Y$
127		simpr	$⊢ ((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \to Z \in (Y L S)$
128	14	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \to Y \neq S$
129	1 2 3 124 121 122 123 126 127 128	lnrot2	$⊢ ((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \to S \in (Z L Y)$
130	1 2 23 121 122 123 124 122 3 129	lnhl	$⊢ ((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \to (S {hl}_{𝒢} (G) (Y) Z \lor Y \in (Z I S))$
131	97 120 130	mpjaodan	$⊢ ((φ \land \neg X \in (Y L S)) \land Z \in (Y L S)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
132		eqid	$⊢ \sim_{𝒢}^{∠} (G) = \sim_{𝒢}^{∠} (G)$
133		eleq1	$⊢ a = c \to (a \in (P ∖ (Y L S)) \leftrightarrow c \in (P ∖ (Y L S)))$
134	133	adantr	$⊢ (a = c \land b = d) \to (a \in (P ∖ (Y L S)) \leftrightarrow c \in (P ∖ (Y L S)))$
135		eleq1	$⊢ b = d \to (b \in (P ∖ (Y L S)) \leftrightarrow d \in (P ∖ (Y L S)))$
136	135	adantl	$⊢ (a = c \land b = d) \to (b \in (P ∖ (Y L S)) \leftrightarrow d \in (P ∖ (Y L S)))$
137	134 136	anbi12d	$⊢ (a = c \land b = d) \to ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \leftrightarrow (c \in (P ∖ (Y L S)) \land d \in (P ∖ (Y L S))))$
138		oveq12	$⊢ (a = c \land b = d) \to a I b = c I d$
139	138	eleq2d	$⊢ (a = c \land b = d) \to (s \in (a I b) \leftrightarrow s \in (c I d))$
140	139	rexbidv	$⊢ (a = c \land b = d) \to (\exists s \in (Y L S) s \in (a I b) \leftrightarrow \exists s \in (Y L S) s \in (c I d))$
141		eleq1	$⊢ s = t \to (s \in (c I d) \leftrightarrow t \in (c I d))$
142	141	cbvrexvw	$⊢ \exists s \in (Y L S) s \in (c I d) \leftrightarrow \exists t \in (Y L S) t \in (c I d)$
143	140 142	bitrdi	$⊢ (a = c \land b = d) \to (\exists s \in (Y L S) s \in (a I b) \leftrightarrow \exists t \in (Y L S) t \in (c I d))$
144	137 143	anbi12d	$⊢ (a = c \land b = d) \to (((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b)) \leftrightarrow ((c \in (P ∖ (Y L S)) \land d \in (P ∖ (Y L S))) \land \exists t \in (Y L S) t \in (c I d)))$
145	144	cbvopabv	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b))\} = \{⟨c, d⟩ \| ((c \in (P ∖ (Y L S)) \land d \in (P ∖ (Y L S))) \land \exists t \in (Y L S) t \in (c I d))\}$
146		eleq1	$⊢ e = g \to (e \in (P ∖ (V L T)) \leftrightarrow g \in (P ∖ (V L T)))$
147	146	adantr	$⊢ (e = g \land f = h) \to (e \in (P ∖ (V L T)) \leftrightarrow g \in (P ∖ (V L T)))$
148		eleq1	$⊢ f = h \to (f \in (P ∖ (V L T)) \leftrightarrow h \in (P ∖ (V L T)))$
149	148	adantl	$⊢ (e = g \land f = h) \to (f \in (P ∖ (V L T)) \leftrightarrow h \in (P ∖ (V L T)))$
150	147 149	anbi12d	$⊢ (e = g \land f = h) \to ((e \in (P ∖ (V L T)) \land f \in (P ∖ (V L T))) \leftrightarrow (g \in (P ∖ (V L T)) \land h \in (P ∖ (V L T))))$
151		oveq12	$⊢ (e = g \land f = h) \to e I f = g I h$
152	151	eleq2d	$⊢ (e = g \land f = h) \to (u \in (e I f) \leftrightarrow u \in (g I h))$
153	152	rexbidv	$⊢ (e = g \land f = h) \to (\exists u \in (V L T) u \in (e I f) \leftrightarrow \exists u \in (V L T) u \in (g I h))$
154		eleq1	$⊢ u = v \to (u \in (g I h) \leftrightarrow v \in (g I h))$
155	154	cbvrexvw	$⊢ \exists u \in (V L T) u \in (g I h) \leftrightarrow \exists v \in (V L T) v \in (g I h)$
156	153 155	bitrdi	$⊢ (e = g \land f = h) \to (\exists u \in (V L T) u \in (e I f) \leftrightarrow \exists v \in (V L T) v \in (g I h))$
157	150 156	anbi12d	$⊢ (e = g \land f = h) \to (((e \in (P ∖ (V L T)) \land f \in (P ∖ (V L T))) \land \exists u \in (V L T) u \in (e I f)) \leftrightarrow ((g \in (P ∖ (V L T)) \land h \in (P ∖ (V L T))) \land \exists v \in (V L T) v \in (g I h)))$
158	157	cbvopabv	$⊢ \{⟨e, f⟩ \| ((e \in (P ∖ (V L T)) \land f \in (P ∖ (V L T))) \land \exists u \in (V L T) u \in (e I f))\} = \{⟨g, h⟩ \| ((g \in (P ∖ (V L T)) \land h \in (P ∖ (V L T))) \land \exists v \in (V L T) v \in (g I h))\}$
159	5	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to G \in 𝒢_{Tarski}$
160	6	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to S \in P$
161	7	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to T \in P$
162	8	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to U \in P$
163	9	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to V \in P$
164	10	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to W \in P$
165	11	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to X \in P$
166	12	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to Y \in P$
167	13	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to Z \in P$
168	14	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to Y \neq S$
169	15	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to V \neq T$
170		simplr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to \neg X \in (Y L S)$
171	165 170	eldifd	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to X \in (P ∖ (Y L S))$
172		simpr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to \neg Z \in (Y L S)$
173	167 172	eldifd	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to Z \in (P ∖ (Y L S))$
174	171 173	jca	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to (X \in (P ∖ (Y L S)) \land Z \in (P ∖ (Y L S)))$
175		inn0	$⊢ (Y L S) \cap (X I Z) \neq \emptyset \leftrightarrow \exists t \in (Y L S) t \in (X I Z)$
176	16 175	sylib	$⊢ φ \to \exists t \in (Y L S) t \in (X I Z)$
177	176	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to \exists t \in (Y L S) t \in (X I Z)$
178	174 177	jca	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to ((X \in (P ∖ (Y L S)) \land Z \in (P ∖ (Y L S))) \land \exists t \in (Y L S) t \in (X I Z))$
179	145	a1i	$⊢ φ \to \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b))\} = \{⟨c, d⟩ \| ((c \in (P ∖ (Y L S)) \land d \in (P ∖ (Y L S))) \land \exists t \in (Y L S) t \in (c I d))\}$
180		oveq12	$⊢ (c = X \land d = Z) \to c I d = X I Z$
181	180	eleq2d	$⊢ (c = X \land d = Z) \to (t \in (c I d) \leftrightarrow t \in (X I Z))$
182	181	adantl	$⊢ (φ \land (c = X \land d = Z)) \to (t \in (c I d) \leftrightarrow t \in (X I Z))$
183	182	rexbidv	$⊢ (φ \land (c = X \land d = Z)) \to (\exists t \in (Y L S) t \in (c I d) \leftrightarrow \exists t \in (Y L S) t \in (X I Z))$
184	179 183	brab2d	$⊢ φ \to (X \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b))\} Z \leftrightarrow ((X \in (P ∖ (Y L S)) \land Z \in (P ∖ (Y L S))) \land \exists t \in (Y L S) t \in (X I Z)))$
185	184	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to (X \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b))\} Z \leftrightarrow ((X \in (P ∖ (Y L S)) \land Z \in (P ∖ (Y L S))) \land \exists t \in (Y L S) t \in (X I Z)))$
186	178 185	mpbird	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to X \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b))\} Z$
187		simpr	$⊢ (φ \land \neg X \in (Y L S)) \to \neg X \in (Y L S)$
188	5	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to G \in 𝒢_{Tarski}$
189	12	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to Y \in P$
190	6	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to S \in P$
191	11	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to X \in P$
192	14	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to Y \neq S$
193	8	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to U \in P$
194	9	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to V \in P$
195	7	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to T \in P$
196	63	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to ⟨“ U V T ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y S ”⟩$
197		animorrl	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to (U \in (V L T) \lor V = T)$
198	1 3 2 188 194 195 193 197	colrot2	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to (T \in (U L V) \lor U = V)$
199	1 2 34 188 193 194 195 191 189 190 196 3 198	cgracol	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to (S \in (X L Y) \lor X = Y)$
200	60	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to X \neq Y$
201	200	neneqd	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to \neg X = Y$
202	199 201	olcnd	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to S \in (X L Y)$
203	1 2 3 188 189 190 191 192 202 200	lnrot1	$⊢ ((φ \land \neg X \in (Y L S)) \land U \in (V L T)) \to X \in (Y L S)$
204	187 203	mtand	$⊢ (φ \land \neg X \in (Y L S)) \to \neg U \in (V L T)$
205	204	adantr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to \neg U \in (V L T)$
206	162 205	eldifd	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to U \in (P ∖ (V L T))$
207		simpr	$⊢ (φ \land \neg Z \in (Y L S)) \to \neg Z \in (Y L S)$
208	5	ad2antrr	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to G \in 𝒢_{Tarski}$
209	12	ad2antrr	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to Y \in P$
210	6	ad2antrr	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to S \in P$
211	13	ad2antrr	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to Z \in P$
212	14	ad2antrr	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to Y \neq S$
213	7	ad2antrr	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to T \in P$
214	9	ad2antrr	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to V \in P$
215	10	ad2antrr	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to W \in P$
216	115	ad2antrr	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to ⟨“ T V W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ S Y Z ”⟩$
217		animorrl	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to (W \in (V L T) \lor V = T)$
218	1 3 2 208 214 213 215 217	colcom	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to (W \in (T L V) \lor T = V)$
219	1 2 34 208 213 214 215 210 209 211 216 3 218	cgracol	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to (Z \in (S L Y) \lor S = Y)$
220	14	necomd	$⊢ φ \to S \neq Y$
221	220	neneqd	$⊢ φ \to \neg S = Y$
222	221	ad2antrr	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to \neg S = Y$
223	219 222	olcnd	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to Z \in (S L Y)$
224	1 2 3 208 209 210 211 212 223	lncom	$⊢ ((φ \land \neg Z \in (Y L S)) \land W \in (V L T)) \to Z \in (Y L S)$
225	207 224	mtand	$⊢ (φ \land \neg Z \in (Y L S)) \to \neg W \in (V L T)$
226	225	adantlr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to \neg W \in (V L T)$
227	164 226	eldifd	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to W \in (P ∖ (V L T))$
228	206 227	jca	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to (U \in (P ∖ (V L T)) \land W \in (P ∖ (V L T)))$
229		inn0	$⊢ (V L T) \cap (U I W) \neq \emptyset \leftrightarrow \exists v \in (V L T) v \in (U I W)$
230	17 229	sylib	$⊢ φ \to \exists v \in (V L T) v \in (U I W)$
231	230	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to \exists v \in (V L T) v \in (U I W)$
232	228 231	jca	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to ((U \in (P ∖ (V L T)) \land W \in (P ∖ (V L T))) \land \exists v \in (V L T) v \in (U I W))$
233	158	a1i	$⊢ φ \to \{⟨e, f⟩ \| ((e \in (P ∖ (V L T)) \land f \in (P ∖ (V L T))) \land \exists u \in (V L T) u \in (e I f))\} = \{⟨g, h⟩ \| ((g \in (P ∖ (V L T)) \land h \in (P ∖ (V L T))) \land \exists v \in (V L T) v \in (g I h))\}$
234		oveq12	$⊢ (g = U \land h = W) \to g I h = U I W$
235	234	eleq2d	$⊢ (g = U \land h = W) \to (v \in (g I h) \leftrightarrow v \in (U I W))$
236	235	adantl	$⊢ (φ \land (g = U \land h = W)) \to (v \in (g I h) \leftrightarrow v \in (U I W))$
237	236	rexbidv	$⊢ (φ \land (g = U \land h = W)) \to (\exists v \in (V L T) v \in (g I h) \leftrightarrow \exists v \in (V L T) v \in (U I W))$
238	233 237	brab2d	$⊢ φ \to (U \{⟨e, f⟩ \| ((e \in (P ∖ (V L T)) \land f \in (P ∖ (V L T))) \land \exists u \in (V L T) u \in (e I f))\} W \leftrightarrow ((U \in (P ∖ (V L T)) \land W \in (P ∖ (V L T))) \land \exists v \in (V L T) v \in (U I W)))$
239	238	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to (U \{⟨e, f⟩ \| ((e \in (P ∖ (V L T)) \land f \in (P ∖ (V L T))) \land \exists u \in (V L T) u \in (e I f))\} W \leftrightarrow ((U \in (P ∖ (V L T)) \land W \in (P ∖ (V L T))) \land \exists v \in (V L T) v \in (U I W)))$
240	232 239	mpbird	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to U \{⟨e, f⟩ \| ((e \in (P ∖ (V L T)) \land f \in (P ∖ (V L T))) \land \exists u \in (V L T) u \in (e I f))\} W$
241	35	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to ⟨“ X Y S ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V T ”⟩$
242	32	ad2antrr	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to ⟨“ S Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ T V W ”⟩$
243	1 2 3 132 145 158 159 160 161 162 163 164 165 166 167 168 169 186 240 241 242	tgaaddcpbl	$⊢ ((φ \land \neg X \in (Y L S)) \land \neg Z \in (Y L S)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
244		exmidd	$⊢ (φ \land \neg X \in (Y L S)) \to (Z \in (Y L S) \lor \neg Z \in (Y L S))$
245	131 243 244	mpjaodan	$⊢ (φ \land \neg X \in (Y L S)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
246		exmidd	$⊢ φ \to (X \in (Y L S) \lor \neg X \in (Y L S))$
247	78 245 246	mpjaodan	$⊢ φ \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
248	21 247	breqdi	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$

Metamath Proof Explorer

Theorem tgaaddcpbl2

Proof