tglnpt4

Description: Find a second point on a line, outside of a second line. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	tglnpt2.p	$⊢ P = {Base}_{G}$
	tglnpt2.i	$⊢ I = Itv (G)$
	tglnpt2.l	$⊢ L = {Line}_{𝒢} (G)$
	tglnpt2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglnpt2.a	$⊢ φ \to A \in ran L$
	tglnpt4.y	$⊢ φ \to B \in ran L$
	tglnpt4.x	$⊢ φ \to X \in A$
	tglnpt4.1	$⊢ φ \to A \neq B$
Assertion	tglnpt4	$⊢ φ \to \exists z \in (A ∖ B) z \neq X$

Proof

Step	Hyp	Ref	Expression
1		tglnpt2.p	$⊢ P = {Base}_{G}$
2		tglnpt2.i	$⊢ I = Itv (G)$
3		tglnpt2.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglnpt2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglnpt2.a	$⊢ φ \to A \in ran L$
6		tglnpt4.y	$⊢ φ \to B \in ran L$
7		tglnpt4.x	$⊢ φ \to X \in A$
8		tglnpt4.1	$⊢ φ \to A \neq B$
9	4	adantr	$⊢ (φ \land X \in B) \to G \in 𝒢_{Tarski}$
10	5	adantr	$⊢ (φ \land X \in B) \to A \in ran L$
11	7	adantr	$⊢ (φ \land X \in B) \to X \in A$
12	1 2 3 9 10 11	tglnpt2	$⊢ (φ \land X \in B) \to \exists z \in A X \neq z$
13		simplr	$⊢ (((φ \land X \in B) \land z \in A) \land X \neq z) \to z \in A$
14		simpr	$⊢ (((φ \land X \in B) \land z \in A) \land X \neq z) \to X \neq z$
15	14	neneqd	$⊢ (((φ \land X \in B) \land z \in A) \land X \neq z) \to \neg X = z$
16	4	ad4antr	$⊢ ((((φ \land X \in B) \land z \in A) \land X \neq z) \land z \in B) \to G \in 𝒢_{Tarski}$
17	5	ad4antr	$⊢ ((((φ \land X \in B) \land z \in A) \land X \neq z) \land z \in B) \to A \in ran L$
18	6	ad4antr	$⊢ ((((φ \land X \in B) \land z \in A) \land X \neq z) \land z \in B) \to B \in ran L$
19	8	ad4antr	$⊢ ((((φ \land X \in B) \land z \in A) \land X \neq z) \land z \in B) \to A \neq B$
20	7	ad4antr	$⊢ ((((φ \land X \in B) \land z \in A) \land X \neq z) \land z \in B) \to X \in A$
21		simp-4r	$⊢ ((((φ \land X \in B) \land z \in A) \land X \neq z) \land z \in B) \to X \in B$
22	20 21	elind	$⊢ ((((φ \land X \in B) \land z \in A) \land X \neq z) \land z \in B) \to X \in (A \cap B)$
23		simpllr	$⊢ ((((φ \land X \in B) \land z \in A) \land X \neq z) \land z \in B) \to z \in A$
24		simpr	$⊢ ((((φ \land X \in B) \land z \in A) \land X \neq z) \land z \in B) \to z \in B$
25	23 24	elind	$⊢ ((((φ \land X \in B) \land z \in A) \land X \neq z) \land z \in B) \to z \in (A \cap B)$
26	1 2 3 16 17 18 19 22 25	tglineineq	$⊢ ((((φ \land X \in B) \land z \in A) \land X \neq z) \land z \in B) \to X = z$
27	15 26	mtand	$⊢ (((φ \land X \in B) \land z \in A) \land X \neq z) \to \neg z \in B$
28	13 27	eldifd	$⊢ (((φ \land X \in B) \land z \in A) \land X \neq z) \to z \in (A ∖ B)$
29	14	necomd	$⊢ (((φ \land X \in B) \land z \in A) \land X \neq z) \to z \neq X$
30	28 29	jca	$⊢ (((φ \land X \in B) \land z \in A) \land X \neq z) \to (z \in (A ∖ B) \land z \neq X)$
31	30	expl	$⊢ (φ \land X \in B) \to ((z \in A \land X \neq z) \to (z \in (A ∖ B) \land z \neq X))$
32	31	reximdv2	$⊢ (φ \land X \in B) \to (\exists z \in A X \neq z \to \exists z \in (A ∖ B) z \neq X)$
33	12 32	mpd	$⊢ (φ \land X \in B) \to \exists z \in (A ∖ B) z \neq X$
34	4	adantr	$⊢ (φ \land A \cap B = \emptyset) \to G \in 𝒢_{Tarski}$
35	5	adantr	$⊢ (φ \land A \cap B = \emptyset) \to A \in ran L$
36	7	adantr	$⊢ (φ \land A \cap B = \emptyset) \to X \in A$
37	1 2 3 34 35 36	tglnpt2	$⊢ (φ \land A \cap B = \emptyset) \to \exists z \in A X \neq z$
38		simplr	$⊢ (((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \to z \in A$
39		simp-4r	$⊢ ((((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \land z \in B) \to A \cap B = \emptyset$
40		simpllr	$⊢ ((((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \land z \in B) \to z \in A$
41		simpr	$⊢ ((((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \land z \in B) \to z \in B$
42	40 41	elind	$⊢ ((((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \land z \in B) \to z \in (A \cap B)$
43	42	ne0d	$⊢ ((((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \land z \in B) \to A \cap B \neq \emptyset$
44	43	neneqd	$⊢ ((((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \land z \in B) \to \neg A \cap B = \emptyset$
45	39 44	pm2.65da	$⊢ (((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \to \neg z \in B$
46	38 45	eldifd	$⊢ (((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \to z \in (A ∖ B)$
47		simpr	$⊢ (((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \to X \neq z$
48	47	necomd	$⊢ (((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \to z \neq X$
49	46 48	jca	$⊢ (((φ \land A \cap B = \emptyset) \land z \in A) \land X \neq z) \to (z \in (A ∖ B) \land z \neq X)$
50	49	expl	$⊢ (φ \land A \cap B = \emptyset) \to ((z \in A \land X \neq z) \to (z \in (A ∖ B) \land z \neq X))$
51	50	reximdv2	$⊢ (φ \land A \cap B = \emptyset) \to (\exists z \in A X \neq z \to \exists z \in (A ∖ B) z \neq X)$
52	37 51	mpd	$⊢ (φ \land A \cap B = \emptyset) \to \exists z \in (A ∖ B) z \neq X$
53	52	adantlr	$⊢ ((φ \land \neg X \in B) \land A \cap B = \emptyset) \to \exists z \in (A ∖ B) z \neq X$
54		simpr	$⊢ ((φ \land \neg X \in B) \land A \cap B \neq \emptyset) \to A \cap B \neq \emptyset$
55	4	ad2antrr	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to G \in 𝒢_{Tarski}$
56	5	ad2antrr	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to A \in ran L$
57	7	ad2antrr	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to X \in A$
58		simpr	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to y \in (A \cap B)$
59	58	elin1d	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to y \in A$
60		simpr	$⊢ (φ \land y \in (A \cap B)) \to y \in (A \cap B)$
61	60	elin2d	$⊢ (φ \land y \in (A \cap B)) \to y \in B$
62	61	adantlr	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to y \in B$
63		simplr	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to \neg X \in B$
64		nelne2	$⊢ (y \in B \land \neg X \in B) \to y \neq X$
65	62 63 64	syl2anc	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to y \neq X$
66	65	necomd	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to X \neq y$
67	1 2 3 55 56 57 59 66	tglnpt3	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to \exists z \in A (z \neq X \land z \neq y)$
68		simpllr	$⊢ ((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \to z \in A$
69		simpr	$⊢ ((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \to z \neq y$
70	69	neneqd	$⊢ ((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \to \neg z = y$
71	4	ad5antr	$⊢ (((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \land z \in B) \to G \in 𝒢_{Tarski}$
72	5	ad5antr	$⊢ (((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \land z \in B) \to A \in ran L$
73	6	ad5antr	$⊢ (((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \land z \in B) \to B \in ran L$
74	8	ad5antr	$⊢ (((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \land z \in B) \to A \neq B$
75	68	adantr	$⊢ (((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \land z \in B) \to z \in A$
76		simpr	$⊢ (((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \land z \in B) \to z \in B$
77	75 76	elind	$⊢ (((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \land z \in B) \to z \in (A \cap B)$
78	60	ad4antr	$⊢ (((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \land z \in B) \to y \in (A \cap B)$
79	1 2 3 71 72 73 74 77 78	tglineineq	$⊢ (((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \land z \in B) \to z = y$
80	70 79	mtand	$⊢ ((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \to \neg z \in B$
81	68 80	eldifd	$⊢ ((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \to z \in (A ∖ B)$
82		simplr	$⊢ ((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \to z \neq X$
83	81 82	jca	$⊢ ((((φ \land y \in (A \cap B)) \land z \in A) \land z \neq X) \land z \neq y) \to (z \in (A ∖ B) \land z \neq X)$
84	83	anasss	$⊢ (((φ \land y \in (A \cap B)) \land z \in A) \land (z \neq X \land z \neq y)) \to (z \in (A ∖ B) \land z \neq X)$
85	84	expl	$⊢ (φ \land y \in (A \cap B)) \to ((z \in A \land (z \neq X \land z \neq y)) \to (z \in (A ∖ B) \land z \neq X))$
86	85	reximdv2	$⊢ (φ \land y \in (A \cap B)) \to (\exists z \in A (z \neq X \land z \neq y) \to \exists z \in (A ∖ B) z \neq X)$
87	86	adantlr	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to (\exists z \in A (z \neq X \land z \neq y) \to \exists z \in (A ∖ B) z \neq X)$
88	67 87	mpd	$⊢ ((φ \land \neg X \in B) \land y \in (A \cap B)) \to \exists z \in (A ∖ B) z \neq X$
89	88	adantlr	$⊢ (((φ \land \neg X \in B) \land A \cap B \neq \emptyset) \land y \in (A \cap B)) \to \exists z \in (A ∖ B) z \neq X$
90	54 89	n0limd	$⊢ ((φ \land \neg X \in B) \land A \cap B \neq \emptyset) \to \exists z \in (A ∖ B) z \neq X$
91	53 90	pm2.61dane	$⊢ (φ \land \neg X \in B) \to \exists z \in (A ∖ B) z \neq X$
92	33 91	pm2.61dan	$⊢ φ \to \exists z \in (A ∖ B) z \neq X$

Metamath Proof Explorer

Theorem tglnpt4

Proof