prlngmolem1

Description: Lemma for prlngmo : Contradiction: Assuming two different parallels B and C having a common point X exist to a line A , the geometry cannot be Euclidean (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlngeu.p	$⊢ P = {Base}_{G}$
	prlngeu.l	$⊢ L = {Line}_{𝒢} (G)$
	prlngeu.r	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	prlngeu.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	prlngeu.a	$⊢ φ \to A \in ran L$
	prlngeu.x	$⊢ φ \to X \in (P ∖ A)$
	prlngmolem1.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ B) \land b \in (P ∖ B)) \land \exists y \in B y \in (a I b))\}$
	prlngmolem1.q	$⊢ Q = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists w \in A w \in (a I b))\}$
	prlngmolem1.i	$⊢ I = Itv (G)$
	prlngmolem1.b	$⊢ φ \to B \in ran L$
	prlngmolem1.c	$⊢ φ \to C \in ran L$
	prlngmolem1.1	$⊢ φ \to A \underset{˙}{∥} B$
	prlngmolem1.2	$⊢ φ \to A \underset{˙}{∥} C$
	prlngmolem1.3	$⊢ φ \to X \in B$
	prlngmolem1.4	$⊢ φ \to X \in C$
	prlngmolem1.t	$⊢ φ \to T \in A$
	prlngmolem1.w	$⊢ φ \to W \in (C ∖ B)$
	prlngmolem1.5	$⊢ φ \to B \neq C$
	prlngmolem1.6	$⊢ φ \to W O T$
Assertion	prlngmolem1	$⊢ φ \to \neg G \in 𝒢_{Tarski}^{E}$

Proof

Step	Hyp	Ref	Expression
1		prlngeu.p	$⊢ P = {Base}_{G}$
2		prlngeu.l	$⊢ L = {Line}_{𝒢} (G)$
3		prlngeu.r	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
4		prlngeu.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		prlngeu.a	$⊢ φ \to A \in ran L$
6		prlngeu.x	$⊢ φ \to X \in (P ∖ A)$
7		prlngmolem1.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ B) \land b \in (P ∖ B)) \land \exists y \in B y \in (a I b))\}$
8		prlngmolem1.q	$⊢ Q = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists w \in A w \in (a I b))\}$
9		prlngmolem1.i	$⊢ I = Itv (G)$
10		prlngmolem1.b	$⊢ φ \to B \in ran L$
11		prlngmolem1.c	$⊢ φ \to C \in ran L$
12		prlngmolem1.1	$⊢ φ \to A \underset{˙}{∥} B$
13		prlngmolem1.2	$⊢ φ \to A \underset{˙}{∥} C$
14		prlngmolem1.3	$⊢ φ \to X \in B$
15		prlngmolem1.4	$⊢ φ \to X \in C$
16		prlngmolem1.t	$⊢ φ \to T \in A$
17		prlngmolem1.w	$⊢ φ \to W \in (C ∖ B)$
18		prlngmolem1.5	$⊢ φ \to B \neq C$
19		prlngmolem1.6	$⊢ φ \to W O T$
20	4	ad5antr	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to G \in 𝒢_{Tarski}$
21	20	ad3antrrr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to G \in 𝒢_{Tarski}$
22	21	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to G \in 𝒢_{Tarski}$
23	5	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to A \in ran L$
24	23	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to A \in ran L$
25		simp-5r	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to r \in P$
26	6	eldifad	$⊢ φ \to X \in P$
27	26	ad5antr	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to X \in P$
28	27	ad3antrrr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to X \in P$
29	28	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to X \in P$
30		eqid	Could not format ( PlnG ` G ) = ( PlnG ` G ) : No typesetting found for \|- ( PlnG ` G ) = ( PlnG ` G ) with typecode \|-
31	12	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to A \underset{˙}{∥} B$
32	31	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to A \underset{˙}{∥} B$
33	6	eldifbd	$⊢ φ \to \neg X \in A$
34		nelne1	$⊢ (X \in B \land \neg X \in A) \to B \neq A$
35	14 33 34	syl2anc	$⊢ φ \to B \neq A$
36	35	necomd	$⊢ φ \to A \neq B$
37	36	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to A \neq B$
38	37	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to A \neq B$
39	10	ad5antr	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to B \in ran L$
40		simp-5r	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to y \in B$
41	1 2 9 20 39 40	tglnpt	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to y \in P$
42	41	ad3antrrr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to y \in P$
43	42	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to y \in P$
44		nelne1	$⊢ (X \in C \land \neg X \in A) \to C \neq A$
45	15 33 44	syl2anc	$⊢ φ \to C \neq A$
46	45	necomd	$⊢ φ \to A \neq C$
47	2 3 4 13 46	prlngin0	$⊢ φ \to A \cap C = \emptyset$
48	47	ad9antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to A \cap C = \emptyset$
49	16	ad9antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to T \in A$
50	21	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to G \in 𝒢_{Tarski}$
51	17	eldifad	$⊢ φ \to W \in C$
52	1 2 9 4 11 51	tglnpt	$⊢ φ \to W \in P$
53	52	ad5antr	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to W \in P$
54	53	ad4antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to W \in P$
55	28	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to X \in P$
56	1 2 9 4 5 16	tglnpt	$⊢ φ \to T \in P$
57	56	ad5antr	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to T \in P$
58	57	ad4antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to T \in P$
59	17	eldifbd	$⊢ φ \to \neg W \in B$
60		nelne2	$⊢ (X \in B \land \neg W \in B) \to X \neq W$
61	14 59 60	syl2anc	$⊢ φ \to X \neq W$
62	61	necomd	$⊢ φ \to W \neq X$
63	62	ad9antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to W \neq X$
64		simpr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to X = y$
65		simp-4r	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to y \in (W I T)$
66	65	ad4antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to y \in (W I T)$
67	64 66	eqeltrd	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to X \in (W I T)$
68	1 9 2 50 54 55 58 63 67	btwnlng3	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to T \in (W L X)$
69	1 9 2 4 52 26 62 62 11 51 15	tglinethru	$⊢ φ \to C = W L X$
70	69	ad9antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to C = W L X$
71	68 70	eleqtrrd	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to T \in C$
72	49 71	elind	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to T \in (A \cap C)$
73	72	ne0d	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to A \cap C \neq \emptyset$
74	73	neneqd	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X = y) \to \neg A \cap C = \emptyset$
75	48 74	pm2.65da	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to \neg X = y$
76	75	neqned	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to X \neq y$
77	76	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to X \neq y$
78		simpllr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to y \in (X I r)$
79	1 9 2 22 29 43 25 77 78	btwnlng3	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to r \in (X L y)$
80	39	ad3antrrr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to B \in ran L$
81	14	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to X \in B$
82	40	ad3antrrr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to y \in B$
83	1 9 2 21 28 42 76 76 80 81 82	tglinethru	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to B = X L y$
84	83	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to B = X L y$
85	79 84	eleqtrrd	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to r \in B$
86	81	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to X \in B$
87	2 30 3 22 32 38 85 86	prlnghpg	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to r {hp}_{𝒢} (G) (A) X$
88		simp-4r	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to s \in P$
89	13	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to A \underset{˙}{∥} C$
90	89	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to A \underset{˙}{∥} C$
91	46	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to A \neq C$
92	91	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to A \neq C$
93	15	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to X \in C$
94	93	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to X \in C$
95		simpllr	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to v \in P$
96	95	ad3antrrr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to v \in P$
97	96	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to v \in P$
98		simp-4r	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to X \neq v$
99	98	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to X \neq v$
100		simplr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to v \in (X I s)$
101	1 9 2 22 29 97 88 99 100	btwnlng3	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to s \in (X L v)$
102	11	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to C \in ran L$
103	20	ad2antrr	$⊢ (((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \to G \in 𝒢_{Tarski}$
104	53	ad2antrr	$⊢ (((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \to W \in P$
105	27	ad2antrr	$⊢ (((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \to X \in P$
106	95	ad2antrr	$⊢ (((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \to v \in P$
107	62	ad7antr	$⊢ (((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \to W \neq X$
108		simplr	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to X \in (W I v)$
109	108	ad2antrr	$⊢ (((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \to X \in (W I v)$
110	1 9 2 103 104 105 106 107 109	btwnlng3	$⊢ (((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \to v \in (W L X)$
111	69	ad7antr	$⊢ (((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \to C = W L X$
112	110 111	eleqtrrd	$⊢ (((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \to v \in C$
113	112	adantr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to v \in C$
114	1 9 2 21 28 96 98 98 102 93 113	tglinethru	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to C = X L v$
115	114	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to C = X L v$
116	101 115	eleqtrrd	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to s \in C$
117	2 30 3 22 90 92 94 116	prlnghpg	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to X {hp}_{𝒢} (G) (A) s$
118	1 9 2 22 24 25 8 29 87 88 117	hpgtr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to r {hp}_{𝒢} (G) (A) s$
119	118	3anasss	$⊢ (((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land (y \in (X I r) \land v \in (X I s) \land T \in (r I s))) \to r {hp}_{𝒢} (G) (A) s$
120		eqid	$⊢ dist (G) = dist (G)$
121	16	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to T \in A$
122	121	ad5antr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to T \in A$
123	1 9 2 8 22 24 25 29 87	hpgne1	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to \neg r \in A$
124	2 30 3 22 90 92 116 94	prlnghpg	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to s {hp}_{𝒢} (G) (A) X$
125	1 9 2 8 22 24 88 29 124	hpgne1	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to \neg s \in A$
126		simpr	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to T \in (r I s)$
127	1 120 9 8 25 88 122 123 125 126	islnoppd	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to r Q s$
128	1 9 2 8 22 24 25 88 127	lnoppnhpg	$⊢ (((((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land y \in (X I r)) \land v \in (X I s)) \land T \in (r I s)) \to \neg r {hp}_{𝒢} (G) (A) s$
129	128	3anasss	$⊢ (((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \land (y \in (X I r) \land v \in (X I s) \land T \in (r I s))) \to \neg r {hp}_{𝒢} (G) (A) s$
130	119 129	pm2.65da	$⊢ ((((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land r \in P) \land s \in P) \to \neg (y \in (X I r) \land v \in (X I s) \land T \in (r I s))$
131	130	anasss	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land (r \in P \land s \in P)) \to \neg (y \in (X I r) \land v \in (X I s) \land T \in (r I s))$
132	131	ralrimivva	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to \forall r \in P \forall s \in P \neg (y \in (X I r) \land v \in (X I s) \land T \in (r I s))$
133		ralnex2	$⊢ \forall r \in P \forall s \in P \neg (y \in (X I r) \land v \in (X I s) \land T \in (r I s)) \leftrightarrow \neg \exists r \in P \exists s \in P (y \in (X I r) \land v \in (X I s) \land T \in (r I s))$
134	132 133	sylib	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to \neg \exists r \in P \exists s \in P (y \in (X I r) \land v \in (X I s) \land T \in (r I s))$
135		simpr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to G \in 𝒢_{Tarski}^{E}$
136	28	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to X \in P$
137	21	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to G \in 𝒢_{Tarski}$
138	80	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to B \in ran L$
139	82	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to y \in B$
140	1 2 9 137 138 139	tglnpt	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to y \in P$
141	96	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to v \in P$
142		simpllr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to z \in P$
143	142	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to z \in P$
144	57	ad4antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to T \in P$
145		simplr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to z \in (X I T)$
146		simpllr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to z \in (y I v)$
147	47	ad9antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to A \cap C = \emptyset$
148	16	ad9antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to T \in A$
149	21	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to G \in 𝒢_{Tarski}$
150	104	ad2antrr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to W \in P$
151	42	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to y \in P$
152	57	ad4antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to T \in P$
153	59	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to \neg W \in B$
154		nelne2	$⊢ (y \in B \land \neg W \in B) \to y \neq W$
155	82 153 154	syl2anc	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to y \neq W$
156	155	necomd	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to W \neq y$
157	156	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to W \neq y$
158	65	ad4antr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to y \in (W I T)$
159	1 9 2 149 150 151 152 157 158	btwnlng3	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to T \in (W L y)$
160	104	adantr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to W \in P$
161	81 153	elnelneq2d	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to \neg X = W$
162	21	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land W = v) \to G \in 𝒢_{Tarski}$
163	160	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land W = v) \to W \in P$
164	28	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land W = v) \to X \in P$
165	109	ad2antrr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land W = v) \to X \in (W I v)$
166		simpr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land W = v) \to W = v$
167	166	oveq2d	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land W = v) \to W I W = W I v$
168	165 167	eleqtrrd	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land W = v) \to X \in (W I W)$
169	1 120 9 162 163 164 168	axtgbtwnid	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land W = v) \to W = X$
170	169	eqcomd	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land W = v) \to X = W$
171	161 170	mtand	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to \neg W = v$
172	171	neqned	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to W \neq v$
173	51	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to W \in C$
174	1 9 2 21 160 96 172 172 102 173 113	tglinethru	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to C = W L v$
175	174	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to C = W L v$
176		simpr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to y = v$
177	176	oveq2d	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to W L y = W L v$
178	175 177	eqtr4d	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to C = W L y$
179	159 178	eleqtrrd	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to T \in C$
180	148 179	elind	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to T \in (A \cap C)$
181	180	ne0d	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to A \cap C \neq \emptyset$
182	181	neneqd	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land y = v) \to \neg A \cap C = \emptyset$
183	147 182	pm2.65da	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to \neg y = v$
184	183	neqned	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to y \neq v$
185		simplr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to z \in (y I v)$
186	1 9 2 21 42 96 142 184 185	btwnlng1	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to z \in (y L v)$
187	18	neneqd	$⊢ φ \to \neg B = C$
188	187	ad8antr	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to \neg B = C$
189	21	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to G \in 𝒢_{Tarski}$
190	28	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to X \in P$
191	96	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to v \in P$
192	98	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to X \neq v$
193	42	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to y \in P$
194	76	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to X \neq y$
195	1 9 2 189 190 193 194	tgelrnln	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to X L y \in ran L$
196	1 9 2 189 190 193 194	tglinerflx1	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to X \in (X L y)$
197		simpr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to X \in (y L v)$
198	184	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to y \neq v$
199	1 9 2 189 190 193 191 194 197 198	lnrot2	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to v \in (X L y)$
200	1 9 2 189 190 191 192 192 195 196 199	tglinethru	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to X L y = X L v$
201	83	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to B = X L y$
202	114	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to C = X L v$
203	200 201 202	3eqtr4d	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land X \in (y L v)) \to B = C$
204	188 203	mtand	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to \neg X \in (y L v)$
205		nelne2	$⊢ (z \in (y L v) \land \neg X \in (y L v)) \to z \neq X$
206	186 204 205	syl2anc	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to z \neq X$
207	206	necomd	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to X \neq z$
208	207	adantr	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to X \neq z$
209	1 120 9 135 136 140 141 143 144 145 146 208	axtgeucl	$⊢ (((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \land G \in 𝒢_{Tarski}^{E}) \to \exists r \in P \exists s \in P (y \in (X I r) \land v \in (X I s) \land T \in (r I s))$
210	134 209	mtand	$⊢ ((((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land z \in (y I v)) \land z \in (X I T)) \to \neg G \in 𝒢_{Tarski}^{E}$
211	210	anasss	$⊢ (((((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \land z \in P) \land (z \in (y I v) \land z \in (X I T))) \to \neg G \in 𝒢_{Tarski}^{E}$
212	1 120 9 20 53 41 57 65	tgbtwncom	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to y \in (T I W)$
213	1 120 9 20 53 27 95 108	tgbtwncom	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to X \in (v I W)$
214	1 120 9 20 57 95 53 41 27 212 213	axtgpasch	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to \exists z \in P (z \in (y I v) \land z \in (X I T))$
215	211 214	r19.29a	$⊢ (((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land X \in (W I v)) \land X \neq v) \to \neg G \in 𝒢_{Tarski}^{E}$
216	215	anasss	$⊢ ((((φ \land y \in B) \land y \in (W I T)) \land v \in P) \land (X \in (W I v) \land X \neq v)) \to \neg G \in 𝒢_{Tarski}^{E}$
217	1	fvexi	$⊢ P \in V$
218	217	a1i	$⊢ φ \to P \in V$
219	218 26 52 61	nehash2	$⊢ φ \to 2 \leq \|P\|$
220	1 120 9 4 52 26 219	tgbtwndiff	$⊢ φ \to \exists v \in P (X \in (W I v) \land X \neq v)$
221	220	ad2antrr	$⊢ ((φ \land y \in B) \land y \in (W I T)) \to \exists v \in P (X \in (W I v) \land X \neq v)$
222	216 221	r19.29a	$⊢ ((φ \land y \in B) \land y \in (W I T)) \to \neg G \in 𝒢_{Tarski}^{E}$
223	1 120 9 7 52 56	islnopp	$⊢ φ \to (W O T \leftrightarrow ((\neg W \in B \land \neg T \in B) \land \exists y \in B y \in (W I T)))$
224	19 223	mpbid	$⊢ φ \to ((\neg W \in B \land \neg T \in B) \land \exists y \in B y \in (W I T))$
225	224	simprd	$⊢ φ \to \exists y \in B y \in (W I T)$
226	222 225	r19.29a	$⊢ φ \to \neg G \in 𝒢_{Tarski}^{E}$

Metamath Proof Explorer

Theorem prlngmolem1

Proof