prlngmolem2

	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)$
	prlngeu.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
	prlngmolem2.1	$⊢ O = \{⟨x, y⟩ \| ((x \in (P ∖ b) \land y \in (P ∖ b)) \land \exists r \in b r \in (x Itv (G) y))\}$
	prlngmolem2.2	$⊢ Q = \{⟨x, y⟩ \| ((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y))\}$
Assertion	prlngmolem2	$⊢ φ \to \exists^{*} b \in ran L (A \underset{˙}{∥} b \land X \in b)$

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		prlngeu.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
8		prlngmolem2.1	$⊢ O = \{⟨x, y⟩ \| ((x \in (P ∖ b) \land y \in (P ∖ b)) \land \exists r \in b r \in (x Itv (G) y))\}$
9		prlngmolem2.2	$⊢ Q = \{⟨x, y⟩ \| ((x \in (P ∖ A) \land y \in (P ∖ A)) \land \exists s \in A s \in (x Itv (G) y))\}$
10		anass	$⊢ ((A \underset{˙}{∥} b \land X \in b) \land (A \underset{˙}{∥} c \land X \in c)) \leftrightarrow (A \underset{˙}{∥} b \land (X \in b \land (A \underset{˙}{∥} c \land X \in c)))$
11	4	ad6antr	$⊢ ((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \to G \in 𝒢_{Tarski}$
12	5	ad6antr	$⊢ ((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \to A \in ran L$
13	2 11 12	tglnne0	$⊢ ((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \to A \neq \emptyset$
14		simpr	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b = c) \to b = c$
15	7	ad8antr	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to G \in 𝒢_{Tarski}^{E}$
16	11	ad2antrr	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to G \in 𝒢_{Tarski}$
17	16	ad3antrrr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to G \in 𝒢_{Tarski}$
18	12	ad5antr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to A \in ran L$
19	6	ad8antr	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to X \in (P ∖ A)$
20	19	ad3antrrr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to X \in (P ∖ A)$
21		eqid	$⊢ Itv (G) = Itv (G)$
22		simp-8r	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to b \in ran L$
23	22	ad3antrrr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to b \in ran L$
24		simp-7r	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to c \in ran L$
25	24	ad3antrrr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to c \in ran L$
26		simp-9r	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to A \underset{˙}{∥} b$
27		simp-7r	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to A \underset{˙}{∥} c$
28		simp-8r	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to X \in b$
29		simpllr	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to X \in c$
30	29	ad3antrrr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to X \in c$
31		simp-5r	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to t \in A$
32		simpllr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to w \in (c ∖ b)$
33		simp-4r	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to b \neq c$
34		simpr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to w O t$
35	1 2 3 17 18 20 8 9 21 23 25 26 27 28 30 31 32 33 34	prlngmolem1	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land w O t) \to \neg G \in 𝒢_{Tarski}^{E}$
36	16	ad3antrrr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to G \in 𝒢_{Tarski}$
37	12	ad5antr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to A \in ran L$
38	19	ad3antrrr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to X \in (P ∖ A)$
39	22	ad3antrrr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to b \in ran L$
40	24	ad3antrrr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to c \in ran L$
41		simp-9r	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to A \underset{˙}{∥} b$
42		simp-7r	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to A \underset{˙}{∥} c$
43		simp-8r	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to X \in b$
44	29	ad3antrrr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to X \in c$
45		simp-5r	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to t \in A$
46		eqid	$⊢ dist (G) = dist (G)$
47		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
48		eqid	$⊢ {pInv}_{𝒢} (G) (X) = {pInv}_{𝒢} (G) (X)$
49		simplr	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to w \in (c ∖ b)$
50	49	eldifad	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to w \in c$
51	50	adantr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to w \in c$
52	1 46 21 2 47 36 48 40 44 51	mirln	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to {pInv}_{𝒢} (G) (X) (w) \in c$
53		simpllr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to w \in (c ∖ b)$
54	53	eldifbd	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to \neg w \in b$
55	36	adantr	$⊢ ((((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \land {pInv}_{𝒢} (G) (X) (w) \in b) \to G \in 𝒢_{Tarski}$
56	1 2 21 16 24 29	tglnpt	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to X \in P$
57	56	ad4antr	$⊢ ((((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \land {pInv}_{𝒢} (G) (X) (w) \in b) \to X \in P$
58	16	ad2antrr	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to G \in 𝒢_{Tarski}$
59	24	ad2antrr	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to c \in ran L$
60	1 2 21 58 59 50	tglnpt	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to w \in P$
61	60	ad2antrr	$⊢ ((((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \land {pInv}_{𝒢} (G) (X) (w) \in b) \to w \in P$
62	1 46 21 2 47 55 57 48 61	mirmir	$⊢ ((((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \land {pInv}_{𝒢} (G) (X) (w) \in b) \to {pInv}_{𝒢} (G) (X) ({pInv}_{𝒢} (G) (X) (w)) = w$
63	39	adantr	$⊢ ((((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \land {pInv}_{𝒢} (G) (X) (w) \in b) \to b \in ran L$
64	43	adantr	$⊢ ((((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \land {pInv}_{𝒢} (G) (X) (w) \in b) \to X \in b$
65		simpr	$⊢ ((((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \land {pInv}_{𝒢} (G) (X) (w) \in b) \to {pInv}_{𝒢} (G) (X) (w) \in b$
66	1 46 21 2 47 55 48 63 64 65	mirln	$⊢ ((((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \land {pInv}_{𝒢} (G) (X) (w) \in b) \to {pInv}_{𝒢} (G) (X) ({pInv}_{𝒢} (G) (X) (w)) \in b$
67	62 66	eqeltrrd	$⊢ ((((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \land {pInv}_{𝒢} (G) (X) (w) \in b) \to w \in b$
68	54 67	mtand	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to \neg {pInv}_{𝒢} (G) (X) (w) \in b$
69	52 68	eldifd	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to {pInv}_{𝒢} (G) (X) (w) \in (c ∖ b)$
70		simp-4r	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to b \neq c$
71		simpr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to {pInv}_{𝒢} (G) (X) (w) O t$
72	1 2 3 36 37 38 8 9 21 39 40 41 42 43 44 45 69 70 71	prlngmolem1	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land {pInv}_{𝒢} (G) (X) (w) O t) \to \neg G \in 𝒢_{Tarski}^{E}$
73		eqid	Could not format ( PlnG ` G ) = ( PlnG ` G ) : No typesetting found for \|- ( PlnG ` G ) = ( PlnG ` G ) with typecode \|-
74	22	ad2antrr	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to b \in ran L$
75	49	eldifbd	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to \neg w \in b$
76	60 75	eldifd	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to w \in (P ∖ b)$
77	12	ad4antr	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to A \in ran L$
78	6	ad10antr	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to X \in (P ∖ A)$
79	1 21 2 73 58 77 78	elplnglnid	Could not format ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> A C_ ( A ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> A C_ ( A ( PlnG ` G ) X ) ) with typecode \|-
80		simp-4r	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to t \in A$
81	79 80	sseldd	Could not format ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> t e. ( A ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> t e. ( A ( PlnG ` G ) X ) ) with typecode \|-
82	1 2 73 58 77 78	tgelrnpln	Could not format ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> ( A ( PlnG ` G ) X ) e. ran ( PlnG ` G ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> ( A ( PlnG ` G ) X ) e. ran ( PlnG ` G ) ) with typecode \|-
83		simp-6r	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to A \underset{˙}{∥} c$
84	29	ad2antrr	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to X \in c$
85	6	eldifbd	$⊢ φ \to \neg X \in A$
86	85	ad10antr	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to \neg X \in A$
87		nelne1	$⊢ (X \in c \land \neg X \in A) \to c \neq A$
88	84 86 87	syl2anc	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to c \neq A$
89	88	necomd	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to A \neq c$
90	2 73 3 58 83 89 50 84	prlnghpg	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to w {hp}_{𝒢} (G) (A) X$
91	1 2 73 77 60 78 58 90	hpgssplng	Could not format ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> w e. ( A ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> w e. ( A ( PlnG ` G ) X ) ) with typecode \|-
92	91 75	eldifd	Could not format ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> w e. ( ( A ( PlnG ` G ) X ) \ b ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> w e. ( ( A ( PlnG ` G ) X ) \ b ) ) with typecode \|-
93		simp-8r	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to A \underset{˙}{∥} b$
94		simp-7r	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to X \in b$
95		nelne1	$⊢ (X \in b \land \neg X \in A) \to b \neq A$
96	94 86 95	syl2anc	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to b \neq A$
97	96	necomd	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to A \neq b$
98	2 73 3 58 93 97 94	prlngpln3	Could not format ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> b C_ ( A ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> b C_ ( A ( PlnG ` G ) X ) ) with typecode \|-
99	1 2 73 58 82 74 92 98	plng3p	Could not format ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> ( A ( PlnG ` G ) X ) = ( b ( PlnG ` G ) w ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> ( A ( PlnG ` G ) X ) = ( b ( PlnG ` G ) w ) ) with typecode \|-
100	81 99	eleqtrd	Could not format ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> t e. ( b ( PlnG ` G ) w ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> t e. ( b ( PlnG ` G ) w ) ) with typecode \|-
101	2 3 58 93 97	prlngin0	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to A \cap b = \emptyset$
102	101	adantr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land t \in b) \to A \cap b = \emptyset$
103		simp-5r	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land t \in b) \to t \in A$
104		simpr	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land t \in b) \to t \in b$
105	103 104	elind	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land t \in b) \to t \in (A \cap b)$
106	105	ne0d	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land t \in b) \to A \cap b \neq \emptyset$
107	106	neneqd	$⊢ (((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \land t \in b) \to \neg A \cap b = \emptyset$
108	102 107	pm2.65da	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to \neg t \in b$
109	100 108	eldifd	Could not format ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> t e. ( ( b ( PlnG ` G ) w ) \ b ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ( ( ph /\ b e. ran L ) /\ c e. ran L ) /\ A .\|\| b ) /\ X e. b ) /\ A .\|\| c ) /\ X e. c ) /\ t e. A ) /\ b =/= c ) /\ w e. ( c \ b ) ) /\ w =/= X ) -> t e. ( ( b ( PlnG ` G ) w ) \ b ) ) with typecode \|-
110	1 21 2 73 47 48 8 58 74 76 109 94	plngmiropp	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to (w O t \lor {pInv}_{𝒢} (G) (X) (w) O t)$
111	35 72 110	mpjaodan	$⊢ ((((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \land w \in (c ∖ b)) \land w \neq X) \to \neg G \in 𝒢_{Tarski}^{E}$
112		simpr	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to b \neq c$
113	112	necomd	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to c \neq b$
114	1 21 2 16 24 22 29 113	tglnpt4	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to \exists w \in (c ∖ b) w \neq X$
115	111 114	r19.29a	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to \neg G \in 𝒢_{Tarski}^{E}$
116	15 115	pm2.21dd	$⊢ ((((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \land b \neq c) \to b = c$
117	14 116	pm2.61dane	$⊢ (((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \land t \in A) \to b = c$
118	13 117	n0limd	$⊢ ((((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land A \underset{˙}{∥} c) \land X \in c) \to b = c$
119	118	anasss	$⊢ (((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land (A \underset{˙}{∥} c \land X \in c)) \to b = c$
120	119	anasss	$⊢ ((((φ \land b \in ran L) \land c \in ran L) \land A \underset{˙}{∥} b) \land (X \in b \land (A \underset{˙}{∥} c \land X \in c))) \to b = c$
121	120	anasss	$⊢ (((φ \land b \in ran L) \land c \in ran L) \land (A \underset{˙}{∥} b \land (X \in b \land (A \underset{˙}{∥} c \land X \in c)))) \to b = c$
122	10 121	sylan2b	$⊢ (((φ \land b \in ran L) \land c \in ran L) \land ((A \underset{˙}{∥} b \land X \in b) \land (A \underset{˙}{∥} c \land X \in c))) \to b = c$
123	122	ex	$⊢ ((φ \land b \in ran L) \land c \in ran L) \to (((A \underset{˙}{∥} b \land X \in b) \land (A \underset{˙}{∥} c \land X \in c)) \to b = c)$
124	123	ralrimiva	$⊢ (φ \land b \in ran L) \to \forall c \in ran L (((A \underset{˙}{∥} b \land X \in b) \land (A \underset{˙}{∥} c \land X \in c)) \to b = c)$
125	124	ralrimiva	$⊢ φ \to \forall b \in ran L \forall c \in ran L (((A \underset{˙}{∥} b \land X \in b) \land (A \underset{˙}{∥} c \land X \in c)) \to b = c)$
126		breq2	$⊢ b = c \to (A \underset{˙}{∥} b \leftrightarrow A \underset{˙}{∥} c)$
127		eleq2w	$⊢ b = c \to (X \in b \leftrightarrow X \in c)$
128	126 127	anbi12d	$⊢ b = c \to ((A \underset{˙}{∥} b \land X \in b) \leftrightarrow (A \underset{˙}{∥} c \land X \in c))$
129	128	rmo4	$⊢ \exists^{*} b \in ran L (A \underset{˙}{∥} b \land X \in b) \leftrightarrow \forall b \in ran L \forall c \in ran L (((A \underset{˙}{∥} b \land X \in b) \land (A \underset{˙}{∥} c \land X \in c)) \to b = c)$
130	125 129	sylibr	$⊢ φ \to \exists^{*} b \in ran L (A \underset{˙}{∥} b \land X \in b)$

Metamath Proof Explorer

Theorem prlngmolem2

Proof