tgbtwnconn1lem3

	Ref	Expression
Hypotheses	tgbtwnconn1.p	$⊢ P = {Base}_{G}$
	tgbtwnconn1.i	$⊢ I = Itv (G)$
	tgbtwnconn1.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgbtwnconn1.a	$⊢ φ \to A \in P$
	tgbtwnconn1.b	$⊢ φ \to B \in P$
	tgbtwnconn1.c	$⊢ φ \to C \in P$
	tgbtwnconn1.d	$⊢ φ \to D \in P$
	tgbtwnconn1.1	$⊢ φ \to A \neq B$
	tgbtwnconn1.2	$⊢ φ \to B \in (A I C)$
	tgbtwnconn1.3	$⊢ φ \to B \in (A I D)$
	tgbtwnconn1.m	$⊢ \underset{˙}{-} = dist (G)$
	tgbtwnconn1.e	$⊢ φ \to E \in P$
	tgbtwnconn1.f	$⊢ φ \to F \in P$
	tgbtwnconn1.h	$⊢ φ \to H \in P$
	tgbtwnconn1.j	$⊢ φ \to J \in P$
	tgbtwnconn1.4	$⊢ φ \to D \in (A I E)$
	tgbtwnconn1.5	$⊢ φ \to C \in (A I F)$
	tgbtwnconn1.6	$⊢ φ \to E \in (A I H)$
	tgbtwnconn1.7	$⊢ φ \to F \in (A I J)$
	tgbtwnconn1.8	$⊢ φ \to E \underset{˙}{-} D = C \underset{˙}{-} D$
	tgbtwnconn1.9	$⊢ φ \to C \underset{˙}{-} F = C \underset{˙}{-} D$
	tgbtwnconn1.10	$⊢ φ \to E \underset{˙}{-} H = B \underset{˙}{-} C$
	tgbtwnconn1.11	$⊢ φ \to F \underset{˙}{-} J = B \underset{˙}{-} D$
	tgbtwnconn1.x	$⊢ φ \to X \in P$
	tgbtwnconn1.12	$⊢ φ \to X \in (C I E)$
	tgbtwnconn1.13	$⊢ φ \to X \in (D I F)$
	tgbtwnconn1.14	$⊢ φ \to C \neq E$
Assertion	tgbtwnconn1lem3	$⊢ φ \to D = F$

Proof

Step	Hyp	Ref	Expression
1		tgbtwnconn1.p	$⊢ P = {Base}_{G}$
2		tgbtwnconn1.i	$⊢ I = Itv (G)$
3		tgbtwnconn1.g	$⊢ φ \to G \in 𝒢_{Tarski}$
4		tgbtwnconn1.a	$⊢ φ \to A \in P$
5		tgbtwnconn1.b	$⊢ φ \to B \in P$
6		tgbtwnconn1.c	$⊢ φ \to C \in P$
7		tgbtwnconn1.d	$⊢ φ \to D \in P$
8		tgbtwnconn1.1	$⊢ φ \to A \neq B$
9		tgbtwnconn1.2	$⊢ φ \to B \in (A I C)$
10		tgbtwnconn1.3	$⊢ φ \to B \in (A I D)$
11		tgbtwnconn1.m	$⊢ \underset{˙}{-} = dist (G)$
12		tgbtwnconn1.e	$⊢ φ \to E \in P$
13		tgbtwnconn1.f	$⊢ φ \to F \in P$
14		tgbtwnconn1.h	$⊢ φ \to H \in P$
15		tgbtwnconn1.j	$⊢ φ \to J \in P$
16		tgbtwnconn1.4	$⊢ φ \to D \in (A I E)$
17		tgbtwnconn1.5	$⊢ φ \to C \in (A I F)$
18		tgbtwnconn1.6	$⊢ φ \to E \in (A I H)$
19		tgbtwnconn1.7	$⊢ φ \to F \in (A I J)$
20		tgbtwnconn1.8	$⊢ φ \to E \underset{˙}{-} D = C \underset{˙}{-} D$
21		tgbtwnconn1.9	$⊢ φ \to C \underset{˙}{-} F = C \underset{˙}{-} D$
22		tgbtwnconn1.10	$⊢ φ \to E \underset{˙}{-} H = B \underset{˙}{-} C$
23		tgbtwnconn1.11	$⊢ φ \to F \underset{˙}{-} J = B \underset{˙}{-} D$
24		tgbtwnconn1.x	$⊢ φ \to X \in P$
25		tgbtwnconn1.12	$⊢ φ \to X \in (C I E)$
26		tgbtwnconn1.13	$⊢ φ \to X \in (D I F)$
27		tgbtwnconn1.14	$⊢ φ \to C \neq E$
28	3	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to G \in 𝒢_{Tarski}$
29	13	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to F \in P$
30	7	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to D \in P$
31		simplr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to q \in P$
32	28	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to G \in 𝒢_{Tarski}$
33	30	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to D \in P$
34		simpllr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to q \in P$
35	1 11 2 32 33 34	tgcgrtriv	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to D \underset{˙}{-} D = q \underset{˙}{-} q$
36		simpr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to F = X$
37	24	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to X \in P$
38	37	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to X \in P$
39		eqidd	$⊢ φ \to C \underset{˙}{-} E = C \underset{˙}{-} E$
40		eqidd	$⊢ φ \to X \underset{˙}{-} E = X \underset{˙}{-} E$
41	21	eqcomd	$⊢ φ \to C \underset{˙}{-} D = C \underset{˙}{-} F$
42	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	tgbtwnconn1lem2	$⊢ φ \to E \underset{˙}{-} F = C \underset{˙}{-} D$
43	20 42	eqtr4d	$⊢ φ \to E \underset{˙}{-} D = E \underset{˙}{-} F$
44	1 11 2 3 6 24 12 7 6 24 12 13 25 25 39 40 41 43	tgifscgr	$⊢ φ \to X \underset{˙}{-} D = X \underset{˙}{-} F$
45	44	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to X \underset{˙}{-} D = X \underset{˙}{-} F$
46	45	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to X \underset{˙}{-} D = X \underset{˙}{-} F$
47	36	oveq2d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to X \underset{˙}{-} F = X \underset{˙}{-} X$
48	46 47	eqtrd	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to X \underset{˙}{-} D = X \underset{˙}{-} X$
49	1 11 2 32 38 33 38 48	axtgcgrid	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to X = D$
50	36 49	eqtrd	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to F = D$
51	50	oveq1d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to F \underset{˙}{-} D = D \underset{˙}{-} D$
52	29	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to F \in P$
53		simp-4r	$⊢ ((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \to p \in P$
54	53	ad2antrr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to p \in P$
55	54	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to p \in P$
56		simp-4r	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to r \in P$
57	56	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to r \in P$
58	6	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \in P$
59		simpr	$⊢ (φ \land C = F) \to C = F$
60	3	adantr	$⊢ (φ \land C = F) \to G \in 𝒢_{Tarski}$
61	6	adantr	$⊢ (φ \land C = F) \to C \in P$
62	13	adantr	$⊢ (φ \land C = F) \to F \in P$
63	12	adantr	$⊢ (φ \land C = F) \to E \in P$
64	21 42	eqtr4d	$⊢ φ \to C \underset{˙}{-} F = E \underset{˙}{-} F$
65	64	adantr	$⊢ (φ \land C = F) \to C \underset{˙}{-} F = E \underset{˙}{-} F$
66	1 11 2 60 61 62 63 62 65 59	tgcgreq	$⊢ (φ \land C = F) \to E = F$
67	59 66	eqtr4d	$⊢ (φ \land C = F) \to C = E$
68	27	adantr	$⊢ (φ \land C = F) \to C \neq E$
69	68	neneqd	$⊢ (φ \land C = F) \to \neg C = E$
70	67 69	pm2.65da	$⊢ φ \to \neg C = F$
71	70	neqned	$⊢ φ \to C \neq F$
72	71	necomd	$⊢ φ \to F \neq C$
73	72	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to F \neq C$
74		simpllr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)$
75	74	simpld	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \in (F I r)$
76	12	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to E \in P$
77	1 11 2 3 6 24 12 25	tgbtwncom	$⊢ φ \to X \in (E I C)$
78	77	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to X \in (E I C)$
79		simp-5r	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)$
80	79	simpld	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \in (E I p)$
81	1 11 2 28 76 37 58 54 78 80	tgbtwnexch3	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \in (X I p)$
82	1 11 2 28 37 58 54 81	tgbtwncom	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \in (p I X)$
83	79	simprd	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \underset{˙}{-} p = C \underset{˙}{-} F$
84	83	eqcomd	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \underset{˙}{-} F = C \underset{˙}{-} p$
85	1 11 2 28 58 29 58 54 84	tgcgrcomlr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to F \underset{˙}{-} C = p \underset{˙}{-} C$
86	74	simprd	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \underset{˙}{-} r = C \underset{˙}{-} X$
87	1 11 2 28 29 54	axtgcgrrflx	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to F \underset{˙}{-} p = p \underset{˙}{-} F$
88	1 11 2 28 29 58 56 54 58 37 54 29 73 75 82 85 86 87 83	axtg5seg	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to r \underset{˙}{-} p = X \underset{˙}{-} F$
89	88	eqcomd	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to X \underset{˙}{-} F = r \underset{˙}{-} p$
90	1 11 2 28 37 29 56 54 89	tgcgrcomlr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to F \underset{˙}{-} X = p \underset{˙}{-} r$
91	90	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to F \underset{˙}{-} X = p \underset{˙}{-} r$
92	1 11 2 32 52 38 55 57 91 36	tgcgreq	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to p = r$
93		simprr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to r \underset{˙}{-} q = r \underset{˙}{-} p$
94	93	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to r \underset{˙}{-} q = r \underset{˙}{-} p$
95	92	oveq2d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to r \underset{˙}{-} p = r \underset{˙}{-} r$
96	94 95	eqtrd	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to r \underset{˙}{-} q = r \underset{˙}{-} r$
97	1 11 2 32 57 34 57 96	axtgcgrid	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to r = q$
98	92 97	eqtrd	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to p = q$
99	98	oveq1d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to p \underset{˙}{-} q = q \underset{˙}{-} q$
100	35 51 99	3eqtr4d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to F \underset{˙}{-} D = p \underset{˙}{-} q$
101	28	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to G \in 𝒢_{Tarski}$
102	29	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to F \in P$
103	37	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to X \in P$
104	30	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to D \in P$
105	54	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to p \in P$
106	56	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to r \in P$
107		simpllr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to q \in P$
108	1 11 2 3 7 24 13 26	tgbtwncom	$⊢ φ \to X \in (F I D)$
109	108	ad7antr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to X \in (F I D)$
110		simplrl	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to r \in (p I q)$
111	90	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to F \underset{˙}{-} X = p \underset{˙}{-} r$
112	88 93 45	3eqtr4rd	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to X \underset{˙}{-} D = r \underset{˙}{-} q$
113	112	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to X \underset{˙}{-} D = r \underset{˙}{-} q$
114	1 11 2 101 102 103 104 105 106 107 109 110 111 113	tgcgrextend	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to F \underset{˙}{-} D = p \underset{˙}{-} q$
115	100 114	pm2.61dane	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to F \underset{˙}{-} D = p \underset{˙}{-} q$
116		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
117		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
118	27	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \neq E$
119	1 116 2 28 58 54 76 80	btwncolg2	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to (E \in (C {Line}_{𝒢} (G) p) \lor C = p)$
120	21	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \underset{˙}{-} F = C \underset{˙}{-} D$
121	85	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to F \underset{˙}{-} C = p \underset{˙}{-} C$
122	50	oveq1d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to F \underset{˙}{-} C = D \underset{˙}{-} C$
123	98	oveq1d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to p \underset{˙}{-} C = q \underset{˙}{-} C$
124	121 122 123	3eqtr3d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F = X) \to D \underset{˙}{-} C = q \underset{˙}{-} C$
125	58	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to C \in P$
126		simpr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to F \neq X$
127	85	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to F \underset{˙}{-} C = p \underset{˙}{-} C$
128	86	eqcomd	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \underset{˙}{-} X = C \underset{˙}{-} r$
129	1 11 2 28 58 37 58 56 128	tgcgrcomlr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to X \underset{˙}{-} C = r \underset{˙}{-} C$
130	129	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to X \underset{˙}{-} C = r \underset{˙}{-} C$
131	1 11 2 101 102 103 104 105 106 107 125 125 126 109 110 111 113 127 130	axtg5seg	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land F \neq X) \to D \underset{˙}{-} C = q \underset{˙}{-} C$
132	124 131	pm2.61dane	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to D \underset{˙}{-} C = q \underset{˙}{-} C$
133	1 11 2 28 30 58 31 58 132	tgcgrcomlr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \underset{˙}{-} D = C \underset{˙}{-} q$
134	83 120 133	3eqtrd	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \underset{˙}{-} p = C \underset{˙}{-} q$
135	5	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to B \in P$
136	15	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to J \in P$
137	28	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to G \in 𝒢_{Tarski}$
138	136	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to J \in P$
139	58	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to C \in P$
140	1 11 2 3 4 6 13 15 17 19	tgbtwnexch	$⊢ φ \to C \in (A I J)$
141	1 11 2 3 4 5 6 15 9 140	tgbtwnexch3	$⊢ φ \to C \in (B I J)$
142	141	ad7antr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to C \in (B I J)$
143		simpr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to B = J$
144	143	oveq1d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to B I J = J I J$
145	142 144	eleqtrd	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to C \in (J I J)$
146	1 11 2 137 138 139 145	axtgbtwnid	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to J = C$
147	29	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to F \in P$
148	1 11 2 3 4 6 13 15 17 19	tgbtwnexch3	$⊢ φ \to F \in (C I J)$
149	1 11 2 3 5 6 13 15 141 148	tgbtwnexch2	$⊢ φ \to F \in (B I J)$
150	149	ad7antr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to F \in (B I J)$
151	150 144	eleqtrd	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to F \in (J I J)$
152	1 11 2 137 138 147 151	axtgbtwnid	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to J = F$
153	146 152	eqtr3d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to C = F$
154	70	ad7antr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land B = J) \to \neg C = F$
155	153 154	pm2.65da	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to \neg B = J$
156	155	neqned	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to B \neq J$
157	1 11 2 3 4 5 7 12 10 16	tgbtwnexch	$⊢ φ \to B \in (A I E)$
158	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	tgbtwnconn1lem1	$⊢ φ \to H = J$
159	158	oveq2d	$⊢ φ \to A I H = A I J$
160	18 159	eleqtrd	$⊢ φ \to E \in (A I J)$
161	1 11 2 3 4 5 12 15 157 160	tgbtwnexch3	$⊢ φ \to E \in (B I J)$
162	161	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to E \in (B I J)$
163	1 116 2 28 135 76 136 162	btwncolg3	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to (J \in (B {Line}_{𝒢} (G) E) \lor B = E)$
164	71	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \neq F$
165	1 11 2 3 13 6 5 15 148 141	tgbtwnintr	$⊢ φ \to C \in (F I B)$
166	165	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \in (F I B)$
167	1 116 2 28 58 135 29 166	btwncolg2	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to (F \in (C {Line}_{𝒢} (G) B) \lor C = B)$
168	28	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to G \in 𝒢_{Tarski}$
169	58	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to C \in P$
170	56	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to r \in P$
171	37	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to X \in P$
172	86	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to C \underset{˙}{-} r = C \underset{˙}{-} X$
173		simpr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to C = r$
174	1 11 2 168 169 170 169 171 172 173	tgcgreq	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to C = X$
175	76	adantr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to E \in P$
176		eqidd	$⊢ φ \to D \underset{˙}{-} F = D \underset{˙}{-} F$
177		eqidd	$⊢ φ \to X \underset{˙}{-} F = X \underset{˙}{-} F$
178	20	eqcomd	$⊢ φ \to C \underset{˙}{-} D = E \underset{˙}{-} D$
179	1 11 2 3 6 7 12 7 178	tgcgrcomlr	$⊢ φ \to D \underset{˙}{-} C = D \underset{˙}{-} E$
180	1 11 2 3 6 13 12 13 64	tgcgrcomlr	$⊢ φ \to F \underset{˙}{-} C = F \underset{˙}{-} E$
181	1 11 2 3 7 24 13 6 7 24 13 12 26 26 176 177 179 180	tgifscgr	$⊢ φ \to X \underset{˙}{-} C = X \underset{˙}{-} E$
182	181	ad7antr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to X \underset{˙}{-} C = X \underset{˙}{-} E$
183	174	oveq2d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to X \underset{˙}{-} C = X \underset{˙}{-} X$
184	182 183	eqtr3d	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to X \underset{˙}{-} E = X \underset{˙}{-} X$
185	1 11 2 168 171 175 171 184	axtgcgrid	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to X = E$
186	174 185	eqtrd	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to C = E$
187	27	neneqd	$⊢ φ \to \neg C = E$
188	187	ad7antr	$⊢ (((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \land C = r) \to \neg C = E$
189	186 188	pm2.65da	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to \neg C = r$
190	189	neqned	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \neq r$
191	1 11 2 28 29 58 56 75	tgbtwncom	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to C \in (r I F)$
192	1 116 2 28 58 29 56 191	btwncolg2	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to (r \in (C {Line}_{𝒢} (G) F) \lor C = F)$
193	93	eqcomd	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to r \underset{˙}{-} p = r \underset{˙}{-} q$
194	1 116 2 28 58 56 29 117 54 31 11 190 192 134 193	lncgr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to F \underset{˙}{-} p = F \underset{˙}{-} q$
195	1 116 2 28 58 29 135 117 54 31 11 164 167 134 194	lncgr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to B \underset{˙}{-} p = B \underset{˙}{-} q$
196	148	ad6antr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to F \in (C I J)$
197	1 116 2 28 58 136 29 196	btwncolg1	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to (F \in (C {Line}_{𝒢} (G) J) \lor C = J)$
198	1 116 2 28 58 29 136 117 54 31 11 164 197 134 194	lncgr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to J \underset{˙}{-} p = J \underset{˙}{-} q$
199	1 116 2 28 135 136 76 117 54 31 11 156 163 195 198	lncgr	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to E \underset{˙}{-} p = E \underset{˙}{-} q$
200	1 116 2 28 58 76 54 117 31 58 11 118 119 134 199	lnid	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to p = q$
201	200	oveq1d	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to p \underset{˙}{-} q = q \underset{˙}{-} q$
202	115 201	eqtrd	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to F \underset{˙}{-} D = q \underset{˙}{-} q$
203	1 11 2 28 29 30 31 202	axtgcgrid	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to F = D$
204	203	eqcomd	$⊢ ((((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \land q \in P) \land (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)) \to D = F$
205	3	ad2antrr	$⊢ ((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \to G \in 𝒢_{Tarski}$
206	205	ad2antrr	$⊢ ((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \to G \in 𝒢_{Tarski}$
207		simplr	$⊢ ((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \to r \in P$
208	1 11 2 206 53 207 207 53	axtgsegcon	$⊢ ((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \to \exists q \in P (r \in (p I q) \land r \underset{˙}{-} q = r \underset{˙}{-} p)$
209	204 208	r19.29a	$⊢ ((((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \land r \in P) \land (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)) \to D = F$
210	13	ad2antrr	$⊢ ((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \to F \in P$
211	6	ad2antrr	$⊢ ((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \to C \in P$
212	24	ad2antrr	$⊢ ((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \to X \in P$
213	1 11 2 205 210 211 211 212	axtgsegcon	$⊢ ((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \to \exists r \in P (C \in (F I r) \land C \underset{˙}{-} r = C \underset{˙}{-} X)$
214	209 213	r19.29a	$⊢ ((φ \land p \in P) \land (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)) \to D = F$
215	1 11 2 3 12 6 6 13	axtgsegcon	$⊢ φ \to \exists p \in P (C \in (E I p) \land C \underset{˙}{-} p = C \underset{˙}{-} F)$
216	214 215	r19.29a	$⊢ φ \to D = F$

Metamath Proof Explorer

Theorem tgbtwnconn1lem3

Proof