midexlem

Description: Lemma for the existence of a middle point. Lemma 7.25 of Schwabhauser p. 55. This proof of the existence of a midpoint requires the existence of a third point C equidistant to A and B This condition will be removed later. Because the operation notation ( A ( midGG ) B ) for a midpoint implies its uniqueness, it cannot be used until uniqueness is proven, and until then, an equivalent mirror point notation B = ( MA ) has to be used. See mideu for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019)

	Ref	Expression
Hypotheses	mirval.p	$⊢ P = {Base}_{G}$
	mirval.d	$⊢ \underset{˙}{-} = dist (G)$
	mirval.i	$⊢ I = Itv (G)$
	mirval.l	$⊢ L = {Line}_{𝒢} (G)$
	mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
	mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	midexlem.m	$⊢ M = S (x)$
	midexlem.a	$⊢ φ \to A \in P$
	midexlem.b	$⊢ φ \to B \in P$
	midexlem.c	$⊢ φ \to C \in P$
	midexlem.1	$⊢ φ \to C \underset{˙}{-} A = C \underset{˙}{-} B$
Assertion	midexlem	$⊢ φ \to \exists x \in P B = M (A)$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$⊢ P = {Base}_{G}$
2		mirval.d	$⊢ \underset{˙}{-} = dist (G)$
3		mirval.i	$⊢ I = Itv (G)$
4		mirval.l	$⊢ L = {Line}_{𝒢} (G)$
5		mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
6		mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		midexlem.m	$⊢ M = S (x)$
8		midexlem.a	$⊢ φ \to A \in P$
9		midexlem.b	$⊢ φ \to B \in P$
10		midexlem.c	$⊢ φ \to C \in P$
11		midexlem.1	$⊢ φ \to C \underset{˙}{-} A = C \underset{˙}{-} B$
12		fveq2	$⊢ x = C \to S (x) = S (C)$
13	7 12	syl5eq	$⊢ x = C \to M = S (C)$
14	13	fveq1d	$⊢ x = C \to M (A) = S (C) (A)$
15	14	rspceeqv	$⊢ (C \in P \land B = S (C) (A)) \to \exists x \in P B = M (A)$
16	10 15	sylan	$⊢ (φ \land B = S (C) (A)) \to \exists x \in P B = M (A)$
17	16	adantlr	$⊢ ((φ \land (C \in (A L B) \lor A = B)) \land B = S (C) (A)) \to \exists x \in P B = M (A)$
18		eqid	$⊢ S (A) = S (A)$
19	1 2 3 4 5 6 8 18	mircinv	$⊢ φ \to S (A) (A) = A$
20	19	adantr	$⊢ (φ \land A = B) \to S (A) (A) = A$
21		simpr	$⊢ (φ \land A = B) \to A = B$
22	20 21	eqtr2d	$⊢ (φ \land A = B) \to B = S (A) (A)$
23		fveq2	$⊢ x = A \to S (x) = S (A)$
24	7 23	syl5eq	$⊢ x = A \to M = S (A)$
25	24	fveq1d	$⊢ x = A \to M (A) = S (A) (A)$
26	25	rspceeqv	$⊢ (A \in P \land B = S (A) (A)) \to \exists x \in P B = M (A)$
27	8 22 26	syl2an2r	$⊢ (φ \land A = B) \to \exists x \in P B = M (A)$
28	27	adantlr	$⊢ ((φ \land (C \in (A L B) \lor A = B)) \land A = B) \to \exists x \in P B = M (A)$
29	6	adantr	$⊢ (φ \land (C \in (A L B) \lor A = B)) \to G \in 𝒢_{Tarski}$
30		eqid	$⊢ S (C) = S (C)$
31	8	adantr	$⊢ (φ \land (C \in (A L B) \lor A = B)) \to A \in P$
32	9	adantr	$⊢ (φ \land (C \in (A L B) \lor A = B)) \to B \in P$
33	10	adantr	$⊢ (φ \land (C \in (A L B) \lor A = B)) \to C \in P$
34		simpr	$⊢ (φ \land (C \in (A L B) \lor A = B)) \to (C \in (A L B) \lor A = B)$
35	11	adantr	$⊢ (φ \land (C \in (A L B) \lor A = B)) \to C \underset{˙}{-} A = C \underset{˙}{-} B$
36	1 2 3 4 5 29 30 31 32 33 34 35	colmid	$⊢ (φ \land (C \in (A L B) \lor A = B)) \to (B = S (C) (A) \lor A = B)$
37	17 28 36	mpjaodan	$⊢ (φ \land (C \in (A L B) \lor A = B)) \to \exists x \in P B = M (A)$
38	6	adantr	$⊢ (φ \land \neg (C \in (A L B) \lor A = B)) \to G \in 𝒢_{Tarski}$
39	38	ad2antrr	$⊢ (((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \to G \in 𝒢_{Tarski}$
40	39	ad2antrr	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to G \in 𝒢_{Tarski}$
41	40	ad2antrr	$⊢ (((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \to G \in 𝒢_{Tarski}$
42	41	adantr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to G \in 𝒢_{Tarski}$
43		simprl	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to x \in P$
44	8	adantr	$⊢ (φ \land \neg (C \in (A L B) \lor A = B)) \to A \in P$
45	44	ad2antrr	$⊢ (((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \to A \in P$
46	45	ad2antrr	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to A \in P$
47	46	ad2antrr	$⊢ (((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \to A \in P$
48	47	adantr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to A \in P$
49	9	ad3antrrr	$⊢ (((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \to B \in P$
50	49	ad2antrr	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to B \in P$
51	50	ad2antrr	$⊢ (((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \to B \in P$
52	51	adantr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to B \in P$
53	42	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to G \in 𝒢_{Tarski}$
54		simpllr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to r \in P$
55	54	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \in P$
56	10	adantr	$⊢ (φ \land \neg (C \in (A L B) \lor A = B)) \to C \in P$
57	56	ad2antrr	$⊢ (((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \to C \in P$
58	57	ad2antrr	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to C \in P$
59	58	ad2antrr	$⊢ (((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \to C \in P$
60	59	adantr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to C \in P$
61	60	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to C \in P$
62	43	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to x \in P$
63		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
64	52	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to B \in P$
65	48	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to A \in P$
66		simpr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r = A) \to r = A$
67	9	adantr	$⊢ (φ \land \neg (C \in (A L B) \lor A = B)) \to B \in P$
68		simpr	$⊢ (φ \land \neg (C \in (A L B) \lor A = B)) \to \neg (C \in (A L B) \lor A = B)$
69	1 3 4 38 56 44 67 68	ncolne1	$⊢ (φ \land \neg (C \in (A L B) \lor A = B)) \to C \neq A$
70	69	ad7antr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to C \neq A$
71	70	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to C \neq A$
72	71	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r = A) \to C \neq A$
73	72	necomd	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r = A) \to A \neq C$
74	66 73	eqnetrd	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r = A) \to r \neq C$
75	53	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r \neq A) \to G \in 𝒢_{Tarski}$
76	55	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r \neq A) \to r \in P$
77	65	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r \neq A) \to A \in P$
78	61	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r \neq A) \to C \in P$
79		simplr	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to q \in P$
80	79	ad3antrrr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to q \in P$
81	80	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to q \in P$
82	81	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r \neq A) \to q \in P$
83	68	ad9antr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to \neg (C \in (A L B) \lor A = B)$
84	1 4 3 53 65 64 61 83	ncolrot2	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to \neg (B \in (C L A) \lor C = A)$
85	6	adantr	$⊢ (φ \land (C \in (B L A) \lor B = A)) \to G \in 𝒢_{Tarski}$
86	9	adantr	$⊢ (φ \land (C \in (B L A) \lor B = A)) \to B \in P$
87	8	adantr	$⊢ (φ \land (C \in (B L A) \lor B = A)) \to A \in P$
88	10	adantr	$⊢ (φ \land (C \in (B L A) \lor B = A)) \to C \in P$
89		simpr	$⊢ (φ \land (C \in (B L A) \lor B = A)) \to (C \in (B L A) \lor B = A)$
90	1 4 3 85 86 87 88 89	colcom	$⊢ (φ \land (C \in (B L A) \lor B = A)) \to (C \in (A L B) \lor A = B)$
91	90	stoic1a	$⊢ (φ \land \neg (C \in (A L B) \lor A = B)) \to \neg (C \in (B L A) \lor B = A)$
92	91	ad9antr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to \neg (C \in (B L A) \lor B = A)$
93	1 3 4 53 61 64 65 92	ncolne1	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to C \neq B$
94	93	necomd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to B \neq C$
95		simprl	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to B \in (C I q)$
96	95	ad3antrrr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to B \in (C I q)$
97	96	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to B \in (C I q)$
98	1 3 4 53 61 64 81 93 97	btwnlng3	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to q \in (C L B)$
99	1 3 4 53 64 61 81 94 98	lncom	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to q \in (B L C)$
100	53	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land q = C) \to G \in 𝒢_{Tarski}$
101	61	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land q = C) \to C \in P$
102	64	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land q = C) \to B \in P$
103	97	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land q = C) \to B \in (C I q)$
104		simpr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land q = C) \to q = C$
105	104	oveq2d	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land q = C) \to C I q = C I C$
106	103 105	eleqtrd	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land q = C) \to B \in (C I C)$
107	1 2 3 100 101 102 106	axtgbtwnid	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land q = C) \to C = B$
108	93	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land q = C) \to C \neq B$
109	108	neneqd	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land q = C) \to \neg C = B$
110	107 109	pm2.65da	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to \neg q = C$
111	110	neqned	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to q \neq C$
112	1 3 4 53 64 61 65 81 84 99 111	ncolncol	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to \neg (q \in (C L A) \lor C = A)$
113	1 4 3 53 61 65 81 112	ncolcom	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to \neg (q \in (A L C) \lor A = C)$
114	113	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r \neq A) \to \neg (q \in (A L C) \lor A = C)$
115		simp-4r	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to p \in P$
116	115	ad2antrr	$⊢ (((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \to p \in P$
117	116	adantr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to p \in P$
118	117	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to p \in P$
119		simp-4r	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)$
120	119	simprd	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to B \underset{˙}{-} q = A \underset{˙}{-} p$
121	120	eqcomd	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to A \underset{˙}{-} p = B \underset{˙}{-} q$
122	121	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to A \underset{˙}{-} p = B \underset{˙}{-} q$
123	1 2 3 53 65 118 64 81 122	tgcgrcomlr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to p \underset{˙}{-} A = q \underset{˙}{-} B$
124		simpllr	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to (A \in (C I p) \land A \neq p)$
125	124	ad5antr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to (A \in (C I p) \land A \neq p)$
126	125	simprd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to A \neq p$
127	126	necomd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to p \neq A$
128	1 2 3 53 118 65 81 64 123 127	tgcgrneq	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to q \neq B$
129	1 3 4 53 61 64 65 81 92 98 128	ncolncol	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to \neg (q \in (B L A) \lor B = A)$
130	1 3 4 53 81 64 65 129	ncolne2	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to q \neq A$
131	130	necomd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to A \neq q$
132		simp-4r	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to (r \in (A I q) \land r \in (B I p))$
133	132	simpld	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \in (A I q)$
134	1 3 4 53 65 81 55 131 133	btwnlng1	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \in (A L q)$
135	1 3 4 53 81 65 55 130 134	lncom	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \in (q L A)$
136	135	adantr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r \neq A) \to r \in (q L A)$
137		simpr	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r \neq A) \to r \neq A$
138	1 3 4 75 82 77 78 76 114 136 137	ncolncol	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r \neq A) \to \neg (r \in (A L C) \lor A = C)$
139	1 3 4 75 76 77 78 138	ncolne2	$⊢ (((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \land r \neq A) \to r \neq C$
140	74 139	pm2.61dane	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \neq C$
141		simpllr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to (x \in P \land (x \in (A I B) \land x \in (r I C)))$
142	141	simprd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to (x \in (A I B) \land x \in (r I C))$
143	142	simprd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to x \in (r I C)$
144	1 4 3 53 55 62 61 143	btwncolg3	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to (C \in (r L x) \lor r = x)$
145		simplr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to s \in P$
146		simplr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to (r \in (A I q) \land r \in (B I p))$
147	146	simprd	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to r \in (B I p)$
148	147	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \in (B I p)$
149		simprl	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to s \in (A I q)$
150	124	simpld	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to A \in (C I p)$
151	150	ad2antrr	$⊢ (((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \to A \in (C I p)$
152	151	adantr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to A \in (C I p)$
153	11	ad8antr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to C \underset{˙}{-} A = C \underset{˙}{-} B$
154	153	eqcomd	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to C \underset{˙}{-} B = C \underset{˙}{-} A$
155	1 2 3 42 48 52	axtgcgrrflx	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to A \underset{˙}{-} B = B \underset{˙}{-} A$
156	1 2 3 42 60 48 117 60 52 80 52 48 70 152 96 153 121 154 155	axtg5seg	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to p \underset{˙}{-} B = q \underset{˙}{-} A$
157	1 2 3 42 117 52 80 48 156	tgcgrcomlr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to B \underset{˙}{-} p = A \underset{˙}{-} q$
158	157	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to B \underset{˙}{-} p = A \underset{˙}{-} q$
159		simprr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩$
160	1 2 3 63 53 64 55 118 65 145 81 159	cgr3simp2	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \underset{˙}{-} p = s \underset{˙}{-} q$
161	1 2 3 53 64 65	axtgcgrrflx	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to B \underset{˙}{-} A = A \underset{˙}{-} B$
162	1 2 3 53 64 55 118 65 65 145 81 64 148 149 158 160 161 123	tgifscgr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \underset{˙}{-} A = s \underset{˙}{-} B$
163		simp-10l	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to φ$
164	125	simpld	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to A \in (C I p)$
165	1 3 4 53 61 65 118 71 164	btwnlng3	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to p \in (C L A)$
166	1 3 4 53 61 65 64 118 83 165 127	ncolncol	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to \neg (p \in (A L B) \lor A = B)$
167	6	ad2antrr	$⊢ ((φ \land p \in P) \land (B \in (p L A) \lor p = A)) \to G \in 𝒢_{Tarski}$
168		simplr	$⊢ ((φ \land p \in P) \land (B \in (p L A) \lor p = A)) \to p \in P$
169	8	ad2antrr	$⊢ ((φ \land p \in P) \land (B \in (p L A) \lor p = A)) \to A \in P$
170	9	ad2antrr	$⊢ ((φ \land p \in P) \land (B \in (p L A) \lor p = A)) \to B \in P$
171		simpr	$⊢ ((φ \land p \in P) \land (B \in (p L A) \lor p = A)) \to (B \in (p L A) \lor p = A)$
172	1 4 3 167 168 169 170 171	colrot1	$⊢ ((φ \land p \in P) \land (B \in (p L A) \lor p = A)) \to (p \in (A L B) \lor A = B)$
173	172	stoic1a	$⊢ ((φ \land p \in P) \land \neg (p \in (A L B) \lor A = B)) \to \neg (B \in (p L A) \lor p = A)$
174	163 118 166 173	syl21anc	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to \neg (B \in (p L A) \lor p = A)$
175	1 3 4 53 118 65 64 166	ncolne2	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to p \neq B$
176	175	necomd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to B \neq p$
177	176	neneqd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to \neg B = p$
178	1 4 3 53 65 81 55 133	btwncolg1	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to (r \in (A L q) \lor A = q)$
179	1 2 3 53 55 65 145 64 162	tgcgrcomlr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to A \underset{˙}{-} r = B \underset{˙}{-} s$
180	120	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to B \underset{˙}{-} q = A \underset{˙}{-} p$
181	1 2 3 53 118 81	axtgcgrrflx	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to p \underset{˙}{-} q = q \underset{˙}{-} p$
182	1 2 3 53 64 55 118 81 65 145 81 118 148 149 158 160 180 181	tgifscgr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \underset{˙}{-} q = s \underset{˙}{-} p$
183	1 2 3 53 65 145 81 149	tgbtwncom	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to s \in (q I A)$
184	1 2 3 42 52 54 117 147	tgbtwncom	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to r \in (p I B)$
185	184	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \in (p I B)$
186	160	eqcomd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to s \underset{˙}{-} q = r \underset{˙}{-} p$
187	1 2 3 53 145 81 55 118 186	tgcgrcomlr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to q \underset{˙}{-} s = p \underset{˙}{-} r$
188	1 2 3 63 53 64 55 118 65 145 81 159	cgr3simp1	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to B \underset{˙}{-} r = A \underset{˙}{-} s$
189	188	eqcomd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to A \underset{˙}{-} s = B \underset{˙}{-} r$
190	1 2 3 53 65 145 64 55 189	tgcgrcomlr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to s \underset{˙}{-} A = r \underset{˙}{-} B$
191	1 2 3 53 81 145 65 118 55 64 183 185 187 190	tgcgrextend	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to q \underset{˙}{-} A = p \underset{˙}{-} B$
192	1 2 63 53 65 55 81 64 145 118 179 182 191	trgcgr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to ⟨“ A r q ”⟩ \sim_{𝒢} (G) ⟨“ B s p ”⟩$
193	1 4 3 53 65 55 81 63 64 145 118 178 192	lnxfr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to (s \in (B L p) \lor B = p)$
194	193	orcomd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to (B = p \lor s \in (B L p))$
195	194	ord	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to (\neg B = p \to s \in (B L p))$
196	177 195	mpd	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to s \in (B L p)$
197	1 3 4 53 64 118 55 176 148	btwnlng1	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \in (B L p)$
198	1 3 4 53 65 81 145 131 149	btwnlng1	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to s \in (A L q)$
199	1 3 4 53 64 118 65 81 174 196 197 198 134	tglineinteq	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to s = r$
200	199	oveq1d	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to s \underset{˙}{-} B = r \underset{˙}{-} B$
201	162 200	eqtr2d	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to r \underset{˙}{-} B = r \underset{˙}{-} A$
202	154	ad2antrr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to C \underset{˙}{-} B = C \underset{˙}{-} A$
203	1 4 3 53 55 61 62 63 64 65 2 140 144 201 202	lncgr	$⊢ ((((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \land s \in P) \land (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)) \to x \underset{˙}{-} B = x \underset{˙}{-} A$
204	1 2 3 63 42 52 54 117 48 80 147 157	tgcgrxfr	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to \exists s \in P (s \in (A I q) \land ⟨“ B r p ”⟩ \sim_{𝒢} (G) ⟨“ A s q ”⟩)$
205	203 204	r19.29a	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to x \underset{˙}{-} B = x \underset{˙}{-} A$
206		simprrl	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to x \in (A I B)$
207	1 2 3 42 48 43 52 206	tgbtwncom	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to x \in (B I A)$
208	1 2 3 4 5 42 43 7 48 52 205 207	ismir	$⊢ ((((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \land (x \in P \land (x \in (A I B) \land x \in (r I C)))) \to B = M (A)$
209		simplr	$⊢ (((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \to r \in P$
210		simprr	$⊢ (((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \to r \in (B I p)$
211	1 2 3 41 59 51 116 47 209 151 210	axtgpasch	$⊢ (((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \to \exists x \in P (x \in (A I B) \land x \in (r I C))$
212	208 211	reximddv	$⊢ (((((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \land r \in P) \land (r \in (A I q) \land r \in (B I p))) \to \exists x \in P B = M (A)$
213	1 2 3 40 58 46 115 150	tgbtwncom	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to A \in (p I C)$
214	1 2 3 40 58 50 79 95	tgbtwncom	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to B \in (q I C)$
215	1 2 3 40 115 79 58 46 50 213 214	axtgpasch	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to \exists r \in P (r \in (A I q) \land r \in (B I p))$
216	212 215	r19.29a	$⊢ (((((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \land q \in P) \land (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)) \to \exists x \in P B = M (A)$
217		simplr	$⊢ (((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \to p \in P$
218	1 2 3 39 57 49 45 217	axtgsegcon	$⊢ (((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \to \exists q \in P (B \in (C I q) \land B \underset{˙}{-} q = A \underset{˙}{-} p)$
219	216 218	r19.29a	$⊢ (((φ \land \neg (C \in (A L B) \lor A = B)) \land p \in P) \land (A \in (C I p) \land A \neq p)) \to \exists x \in P B = M (A)$
220	1	fvexi	$⊢ P \in V$
221	220	a1i	$⊢ (φ \land \neg (C \in (A L B) \lor A = B)) \to P \in V$
222	221 56 44 69	nehash2	$⊢ (φ \land \neg (C \in (A L B) \lor A = B)) \to 2 \leq \|P\|$
223	1 2 3 38 56 44 222	tgbtwndiff	$⊢ (φ \land \neg (C \in (A L B) \lor A = B)) \to \exists p \in P (A \in (C I p) \land A \neq p)$
224	219 223	r19.29a	$⊢ (φ \land \neg (C \in (A L B) \lor A = B)) \to \exists x \in P B = M (A)$
225	37 224	pm2.61dan	$⊢ φ \to \exists x \in P B = M (A)$

Metamath Proof Explorer

Theorem midexlem

Proof