angmndaddov2lem

	Ref	Expression
Hypotheses	angmndadd.p	$⊢ P = {Base}_{G}$
	angmndadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
	angmndadd.i	$⊢ I = Itv (G)$
	angmndadd.d	$⊢ \underset{˙}{-} = dist (G)$
	angmndadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	angmndadd.l	$⊢ L = {Line}_{𝒢} (G)$
	angmndadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	angmndaddov.u	$⊢ φ \to U \in P$
	angmndaddov.v	$⊢ φ \to V \in P$
	angmndaddov.w	$⊢ φ \to W \in P$
	angmndaddov.x	$⊢ φ \to X \in P$
	angmndaddov.y	$⊢ φ \to Y \in P$
	angmndaddov.z	$⊢ φ \to Z \in P$
	angmndaddeu.1	$⊢ φ \to U \neq V$
	angmndaddeu.2	$⊢ φ \to V \neq W$
	angmndaddeu.3	$⊢ φ \to X \neq Y$
	angmndaddeu.4	$⊢ φ \to Y \neq Z$
	angmndaddov2lem.1	$⊢ φ \to X \in (Y L Z)$
Assertion	angmndaddov2lem	$⊢ φ \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$

Proof

Step	Hyp	Ref	Expression
1		angmndadd.p	$⊢ P = {Base}_{G}$
2		angmndadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
3		angmndadd.i	$⊢ I = Itv (G)$
4		angmndadd.d	$⊢ \underset{˙}{-} = dist (G)$
5		angmndadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
6		angmndadd.l	$⊢ L = {Line}_{𝒢} (G)$
7		angmndadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		angmndaddov.u	$⊢ φ \to U \in P$
9		angmndaddov.v	$⊢ φ \to V \in P$
10		angmndaddov.w	$⊢ φ \to W \in P$
11		angmndaddov.x	$⊢ φ \to X \in P$
12		angmndaddov.y	$⊢ φ \to Y \in P$
13		angmndaddov.z	$⊢ φ \to Z \in P$
14		angmndaddeu.1	$⊢ φ \to U \neq V$
15		angmndaddeu.2	$⊢ φ \to V \neq W$
16		angmndaddeu.3	$⊢ φ \to X \neq Y$
17		angmndaddeu.4	$⊢ φ \to Y \neq Z$
18		angmndaddov2lem.1	$⊢ φ \to X \in (Y L Z)$
19	7	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to G \in 𝒢_{Tarski}$
20	11	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to X \in P$
21	12	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to Y \in P$
22	13	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to Z \in P$
23	8	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to U \in P$
24	9	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to V \in P$
25	10	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to W \in P$
26	16	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to X \neq Y$
27	17	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to Y \neq Z$
28	14	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to U \neq V$
29	15	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to V \neq W$
30		simpr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to U {hl}_{𝒢} (G) (V) W$
31		simplr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to X {hl}_{𝒢} (G) (Y) Z$
32	1 2 3 4 5 6 19 20 21 22 23 24 25 26 27 28 29 30 31	angmndaddeu4	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U {hl}_{𝒢} (G) (V) W) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
33	32	adantlr	$⊢ (((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \land U {hl}_{𝒢} (G) (V) W) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
34	7	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to G \in 𝒢_{Tarski}$
35	11	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to X \in P$
36	12	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to Y \in P$
37	13	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to Z \in P$
38	8	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to U \in P$
39	9	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to V \in P$
40	10	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to W \in P$
41	16	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to X \neq Y$
42	17	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to Y \neq Z$
43	14	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to U \neq V$
44	15	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to V \neq W$
45		simpr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to V \in (W I U)$
46	1 4 3 34 40 39 38 45	tgbtwncom	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to V \in (U I W)$
47		simplr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to X {hl}_{𝒢} (G) (Y) Z$
48	1 2 3 4 5 6 34 35 36 37 38 39 40 41 42 43 44 46 47	angmndaddeu6	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land V \in (W I U)) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
49	48	adantlr	$⊢ (((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \land V \in (W I U)) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
50		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
51	10	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \to W \in P$
52	9	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \to V \in P$
53	8	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \to U \in P$
54	7	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \to G \in 𝒢_{Tarski}$
55	11	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \to X \in P$
56	15	necomd	$⊢ φ \to W \neq V$
57	56	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \to W \neq V$
58		simpr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \to U \in (V L W)$
59	1 3 6 54 51 52 53 57 58	lncom	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \to U \in (W L V)$
60	1 3 50 51 52 53 54 55 6 59	lnhl	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \to (U {hl}_{𝒢} (G) (V) W \lor V \in (W I U))$
61	33 49 60	mpjaodan	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land U \in (V L W)) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
62	7	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to G \in 𝒢_{Tarski}$
63	11	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to X \in P$
64	12	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to Y \in P$
65	13	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to Z \in P$
66	8	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to U \in P$
67	9	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to V \in P$
68	10	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to W \in P$
69	16	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to X \neq Y$
70	17	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to Y \neq Z$
71	14	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to U \neq V$
72	15	ad2antrr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to V \neq W$
73		simpr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to \neg U \in (V L W)$
74		simplr	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to X {hl}_{𝒢} (G) (Y) Z$
75	1 2 3 4 5 6 62 63 64 65 66 67 68 69 70 71 72 73 74	angmndaddeu2	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset)$
76		simpllr	$⊢ ((((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land (V L W) \cap (s I U) \neq \emptyset) \to ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩$
77		simplr	$⊢ ((((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land (V L W) \cap (s I U) \neq \emptyset) \to V \underset{˙}{-} s = Y \underset{˙}{-} X$
78	76 77	jca	$⊢ ((((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land (V L W) \cap (s I U) \neq \emptyset) \to (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
79	78	3anasss	$⊢ ((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset)) \to (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
80		simplr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩$
81		simpr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to V \underset{˙}{-} s = Y \underset{˙}{-} X$
82	62	ad3antrrr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to G \in 𝒢_{Tarski}$
83	67	ad3antrrr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to V \in P$
84	68	ad3antrrr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to W \in P$
85		simpllr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to s \in P$
86	72	ad3antrrr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to V \neq W$
87	63	ad3antrrr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to X \in P$
88	64	ad3antrrr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to Y \in P$
89	65	ad3antrrr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to Z \in P$
90	5	a1i	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
91	90 80	breqdi	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to ⟨“ W V s ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
92	1 3 82 50 84 83 85 87 88 89 91	cgracom	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ W V s ”⟩$
93	74	ad3antrrr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to X {hl}_{𝒢} (G) (Y) Z$
94	1 3 4 82 87 88 89 84 83 85 92 50 93	cgrahl	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to W {hl}_{𝒢} (G) (V) s$
95	1 3 50 84 85 83 82 6 94	hlln	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to W \in (s L V)$
96	81	eqcomd	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to Y \underset{˙}{-} X = V \underset{˙}{-} s$
97	16	necomd	$⊢ φ \to Y \neq X$
98	97	ad5antr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to Y \neq X$
99	1 4 3 82 88 87 83 85 96 98	tgcgrneq	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to V \neq s$
100	99	necomd	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to s \neq V$
101	1 3 6 82 83 84 85 86 95 100	lnrot1	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to s \in (V L W)$
102	66	ad3antrrr	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to U \in P$
103	1 4 3 82 85 102	tgbtwntriv1	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to s \in (s I U)$
104	101 103	elind	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to s \in ((V L W) \cap (s I U))$
105	104	ne0d	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to (V L W) \cap (s I U) \neq \emptyset$
106	80 81 105	3jca	$⊢ (((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset)$
107	106	anasss	$⊢ ((((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \land (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)) \to (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset)$
108	79 107	impbida	$⊢ (((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \land s \in P) \to ((⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset) \leftrightarrow (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X))$
109	108	reubidva	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to (\exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset) \leftrightarrow \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X))$
110	75 109	mpbid	$⊢ ((φ \land X {hl}_{𝒢} (G) (Y) Z) \land \neg U \in (V L W)) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
111		exmidd	$⊢ (φ \land X {hl}_{𝒢} (G) (Y) Z) \to (U \in (V L W) \lor \neg U \in (V L W))$
112	61 110 111	mpjaodan	$⊢ (φ \land X {hl}_{𝒢} (G) (Y) Z) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
113	7	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to G \in 𝒢_{Tarski}$
114	11	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to X \in P$
115	12	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to Y \in P$
116	13	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to Z \in P$
117	8	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to U \in P$
118	9	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to V \in P$
119	10	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to W \in P$
120	16	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to X \neq Y$
121	17	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to Y \neq Z$
122	14	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to U \neq V$
123	15	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to V \neq W$
124		simpr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to U {hl}_{𝒢} (G) (V) W$
125		simplr	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to Y \in (Z I X)$
126	1 4 3 113 116 115 114 125	tgbtwncom	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to Y \in (X I Z)$
127	1 2 3 4 5 6 113 114 115 116 117 118 119 120 121 122 123 124 126	angmndaddeu5	$⊢ ((φ \land Y \in (Z I X)) \land U {hl}_{𝒢} (G) (V) W) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
128	127	adantlr	$⊢ (((φ \land Y \in (Z I X)) \land U \in (V L W)) \land U {hl}_{𝒢} (G) (V) W) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
129	7	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to G \in 𝒢_{Tarski}$
130	11	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to X \in P$
131	12	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to Y \in P$
132	13	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to Z \in P$
133	8	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to U \in P$
134	9	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to V \in P$
135	10	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to W \in P$
136	16	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to X \neq Y$
137	17	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to Y \neq Z$
138	14	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to U \neq V$
139	15	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to V \neq W$
140		simpr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to V \in (W I U)$
141	1 4 3 129 135 134 133 140	tgbtwncom	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to V \in (U I W)$
142		simplr	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to Y \in (Z I X)$
143	1 4 3 129 132 131 130 142	tgbtwncom	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to Y \in (X I Z)$
144	1 2 3 4 5 6 129 130 131 132 133 134 135 136 137 138 139 141 143	angmndaddeu7	$⊢ ((φ \land Y \in (Z I X)) \land V \in (W I U)) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
145	144	adantlr	$⊢ (((φ \land Y \in (Z I X)) \land U \in (V L W)) \land V \in (W I U)) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
146	10	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U \in (V L W)) \to W \in P$
147	9	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U \in (V L W)) \to V \in P$
148	8	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U \in (V L W)) \to U \in P$
149	7	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U \in (V L W)) \to G \in 𝒢_{Tarski}$
150	11	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U \in (V L W)) \to X \in P$
151	56	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land U \in (V L W)) \to W \neq V$
152		simpr	$⊢ ((φ \land Y \in (Z I X)) \land U \in (V L W)) \to U \in (V L W)$
153	1 3 6 149 146 147 148 151 152	lncom	$⊢ ((φ \land Y \in (Z I X)) \land U \in (V L W)) \to U \in (W L V)$
154	1 3 50 146 147 148 149 150 6 153	lnhl	$⊢ ((φ \land Y \in (Z I X)) \land U \in (V L W)) \to (U {hl}_{𝒢} (G) (V) W \lor V \in (W I U))$
155	128 145 154	mpjaodan	$⊢ ((φ \land Y \in (Z I X)) \land U \in (V L W)) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
156	7	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to G \in 𝒢_{Tarski}$
157	11	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to X \in P$
158	12	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to Y \in P$
159	13	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to Z \in P$
160	8	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to U \in P$
161	9	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to V \in P$
162	10	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to W \in P$
163	16	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to X \neq Y$
164	17	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to Y \neq Z$
165	14	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to U \neq V$
166	15	ad2antrr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to V \neq W$
167		simpr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to \neg U \in (V L W)$
168		simplr	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to Y \in (Z I X)$
169	1 4 3 156 159 158 157 168	tgbtwncom	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to Y \in (X I Z)$
170	1 2 3 4 5 6 156 157 158 159 160 161 162 163 164 165 166 167 169	angmndaddeu3	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset)$
171		simpllr	$⊢ ((((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land (V L W) \cap (s I U) \neq \emptyset) \to ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩$
172		simplr	$⊢ ((((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land (V L W) \cap (s I U) \neq \emptyset) \to V \underset{˙}{-} s = Y \underset{˙}{-} X$
173	171 172	jca	$⊢ ((((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land (V L W) \cap (s I U) \neq \emptyset) \to (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
174	173	3anasss	$⊢ ((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset)) \to (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
175		simplr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩$
176		simpr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to V \underset{˙}{-} s = Y \underset{˙}{-} X$
177	156	ad3antrrr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to G \in 𝒢_{Tarski}$
178	161	ad3antrrr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to V \in P$
179	162	ad3antrrr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to W \in P$
180		simpllr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to s \in P$
181	166	ad3antrrr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to V \neq W$
182	56	neneqd	$⊢ φ \to \neg W = V$
183	182	ad5antr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to \neg W = V$
184	177	adantr	$⊢ ((((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land W = s) \to G \in 𝒢_{Tarski}$
185	179	adantr	$⊢ ((((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land W = s) \to W \in P$
186	178	adantr	$⊢ ((((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land W = s) \to V \in P$
187	157	ad3antrrr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to X \in P$
188	158	ad3antrrr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to Y \in P$
189	159	ad3antrrr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to Z \in P$
190	5	a1i	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
191	190 175	breqdi	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to ⟨“ W V s ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
192	1 3 177 50 179 178 180 187 188 189 191	cgracom	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ W V s ”⟩$
193	169	ad3antrrr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to Y \in (X I Z)$
194	1 3 4 177 187 188 189 179 178 180 192 193	cgrabtwn	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to V \in (W I s)$
195	194	adantr	$⊢ ((((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land W = s) \to V \in (W I s)$
196		simpr	$⊢ ((((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land W = s) \to W = s$
197	196	oveq2d	$⊢ ((((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land W = s) \to W I W = W I s$
198	195 197	eleqtrrd	$⊢ ((((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land W = s) \to V \in (W I W)$
199	1 4 3 184 185 186 198	axtgbtwnid	$⊢ ((((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \land W = s) \to W = V$
200	183 199	mtand	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to \neg W = s$
201	200	neqned	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to W \neq s$
202	1 3 6 177 179 180 178 201 194	btwnlng1	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to V \in (W L s)$
203	1 3 6 177 178 179 180 181 202 201	lnrot2	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to s \in (V L W)$
204	160	ad3antrrr	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to U \in P$
205	1 4 3 177 180 204	tgbtwntriv1	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to s \in (s I U)$
206	203 205	elind	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to s \in ((V L W) \cap (s I U))$
207	206	ne0d	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to (V L W) \cap (s I U) \neq \emptyset$
208	175 176 207	3jca	$⊢ (((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land ⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩) \land V \underset{˙}{-} s = Y \underset{˙}{-} X) \to (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset)$
209	208	anasss	$⊢ ((((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \land (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)) \to (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset)$
210	174 209	impbida	$⊢ (((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \land s \in P) \to ((⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset) \leftrightarrow (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X))$
211	210	reubidva	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to (\exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X \land (V L W) \cap (s I U) \neq \emptyset) \leftrightarrow \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X))$
212	170 211	mpbid	$⊢ ((φ \land Y \in (Z I X)) \land \neg U \in (V L W)) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
213		exmidd	$⊢ (φ \land Y \in (Z I X)) \to (U \in (V L W) \lor \neg U \in (V L W))$
214	155 212 213	mpjaodan	$⊢ (φ \land Y \in (Z I X)) \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$
215	17	necomd	$⊢ φ \to Z \neq Y$
216	1 3 6 7 13 12 11 215 18	lncom	$⊢ φ \to X \in (Z L Y)$
217	1 3 50 13 12 11 7 11 6 216	lnhl	$⊢ φ \to (X {hl}_{𝒢} (G) (Y) Z \lor Y \in (Z I X))$
218	112 214 217	mpjaodan	$⊢ φ \to \exists! s \in P (⟨“ W V s ”⟩ \underset{˙}{\sim} ⟨“ X Y Z ”⟩ \land V \underset{˙}{-} s = Y \underset{˙}{-} X)$

Metamath Proof Explorer

Theorem angmndaddov2lem

Proof