prlngmo2

Description: Playfair's axiom, without the restriction that the point X is outside of the line A . Theorem 12.11 of Schwabhauser p. 123. (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	prlngmo2.p	$⊢ P = {Base}_{G}$
	prlngmo2.l	$⊢ L = {Line}_{𝒢} (G)$
	prlngmo2.r	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	prlngmo2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	prlngmo2.a	$⊢ φ \to A \in ran L$
	prlngmo2.x	$⊢ φ \to X \in P$
	prlngmo2.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
Assertion	prlngmo2	$⊢ φ \to \exists^{*} b \in ran L (A \underset{˙}{∥} b \land X \in b)$

Proof

Step	Hyp	Ref	Expression
1		prlngmo2.p	$⊢ P = {Base}_{G}$
2		prlngmo2.l	$⊢ L = {Line}_{𝒢} (G)$
3		prlngmo2.r	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
4		prlngmo2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		prlngmo2.a	$⊢ φ \to A \in ran L$
6		prlngmo2.x	$⊢ φ \to X \in P$
7		prlngmo2.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
8		eqeq2	$⊢ a = A \to (b = a \leftrightarrow b = A)$
9	8	imbi2d	$⊢ a = A \to (((A \underset{˙}{∥} b \land X \in b) \to b = a) \leftrightarrow ((A \underset{˙}{∥} b \land X \in b) \to b = A))$
10	9	ralbidv	$⊢ a = A \to (\forall b \in ran L ((A \underset{˙}{∥} b \land X \in b) \to b = a) \leftrightarrow \forall b \in ran L ((A \underset{˙}{∥} b \land X \in b) \to b = A))$
11	5	adantr	$⊢ (φ \land X \in A) \to A \in ran L$
12	4	ad5antr	$⊢ (((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land \neg b = A) \to G \in 𝒢_{Tarski}$
13		simpllr	$⊢ (((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land \neg b = A) \to A \underset{˙}{∥} b$
14		simpr	$⊢ (((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land \neg b = A) \to \neg b = A$
15	14	neqned	$⊢ (((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land \neg b = A) \to b \neq A$
16	15	necomd	$⊢ (((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land \neg b = A) \to A \neq b$
17	2 3 12 13 16	prlngin0	$⊢ (((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land \neg b = A) \to A \cap b = \emptyset$
18		simp-5r	$⊢ (((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land \neg b = A) \to X \in A$
19		simplr	$⊢ (((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land \neg b = A) \to X \in b$
20	18 19	elind	$⊢ (((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land \neg b = A) \to X \in (A \cap b)$
21	20	ne0d	$⊢ (((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land \neg b = A) \to A \cap b \neq \emptyset$
22	21	neneqd	$⊢ (((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \land \neg b = A) \to \neg A \cap b = \emptyset$
23	17 22	condan	$⊢ ((((φ \land X \in A) \land b \in ran L) \land A \underset{˙}{∥} b) \land X \in b) \to b = A$
24	23	expl	$⊢ ((φ \land X \in A) \land b \in ran L) \to ((A \underset{˙}{∥} b \land X \in b) \to b = A)$
25	24	ralrimiva	$⊢ (φ \land X \in A) \to \forall b \in ran L ((A \underset{˙}{∥} b \land X \in b) \to b = A)$
26	10 11 25	rspcedvdw	$⊢ (φ \land X \in A) \to \exists a \in ran L \forall b \in ran L ((A \underset{˙}{∥} b \land X \in b) \to b = a)$
27		nfv	$⊢ Ⅎ a (A \underset{˙}{∥} b \land X \in b)$
28	27	rmo2i	$⊢ \exists a \in ran L \forall b \in ran L ((A \underset{˙}{∥} b \land X \in b) \to b = a) \to \exists^{*} b \in ran L (A \underset{˙}{∥} b \land X \in b)$
29	26 28	syl	$⊢ (φ \land X \in A) \to \exists^{*} b \in ran L (A \underset{˙}{∥} b \land X \in b)$
30	4	adantr	$⊢ (φ \land \neg X \in A) \to G \in 𝒢_{Tarski}$
31	5	adantr	$⊢ (φ \land \neg X \in A) \to A \in ran L$
32	6	adantr	$⊢ (φ \land \neg X \in A) \to X \in P$
33		simpr	$⊢ (φ \land \neg X \in A) \to \neg X \in A$
34	32 33	eldifd	$⊢ (φ \land \neg X \in A) \to X \in (P ∖ A)$
35	7	adantr	$⊢ (φ \land \neg X \in A) \to G \in 𝒢_{Tarski}^{E}$
36	1 2 3 30 31 34 35	prlngmo	$⊢ (φ \land \neg X \in A) \to \exists^{*} b \in ran L (A \underset{˙}{∥} b \land X \in b)$
37	29 36	pm2.61dan	$⊢ φ \to \exists^{*} b \in ran L (A \underset{˙}{∥} b \land X \in b)$

Metamath Proof Explorer

Theorem prlngmo2

Proof