Theorem prlngmo

Description: Playfair's axiom. Given a line A and a point X not on A , at most one line parallel to A can be drawn through X . Theorem 12.11 of Schwabhauser p. 123. Note that this is the first instance of a theorem where the geometry is required to be Euclidean, as expressed by G e. TarskiGE . Theorem A10 of Schwabhauser p. 24 is used, in the form of axtgeucl , in the proof of prlngmolem1 . See prlngex for the corresponding existence theorem. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlngeu.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	prlngeu.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	prlngeu.r	⊢ ∥ = ( parlnG ‘ 𝐺 )
	prlngeu.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	prlngeu.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	prlngeu.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
	prlngeu.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
Assertion	prlngmo	⊢ ( 𝜑 → ∃* 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )

Proof

Step	Hyp	Ref	Expression
1		prlngeu.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		prlngeu.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
3		prlngeu.r	⊢ ∥ = ( parlnG ‘ 𝐺 )
4		prlngeu.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		prlngeu.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6		prlngeu.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
7		prlngeu.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
8		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ ( 𝑃 ∖ 𝑏 ) ↔ 𝑧 ∈ ( 𝑃 ∖ 𝑏 ) ) )
9		eleq1w	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ ( 𝑃 ∖ 𝑏 ) ↔ 𝑤 ∈ ( 𝑃 ∖ 𝑏 ) ) )
10	8 9	bi2anan9	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ ( 𝑃 ∖ 𝑏 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝑏 ) ) ↔ ( 𝑧 ∈ ( 𝑃 ∖ 𝑏 ) ∧ 𝑤 ∈ ( 𝑃 ∖ 𝑏 ) ) ) )
11		eleq1w	⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) )
12	11	cbvrexvw	⊢ ( ∃ 𝑠 ∈ 𝑏 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑡 ∈ 𝑏 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) )
13		oveq12	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) = ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) )
14	13	eleq2d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ 𝑡 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) )
15	14	rexbidv	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ∃ 𝑡 ∈ 𝑏 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑡 ∈ 𝑏 𝑡 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) )
16	12 15	bitrid	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ∃ 𝑠 ∈ 𝑏 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑡 ∈ 𝑏 𝑡 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) )
17	10 16	anbi12d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝑥 ∈ ( 𝑃 ∖ 𝑏 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝑏 ) ) ∧ ∃ 𝑠 ∈ 𝑏 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) ↔ ( ( 𝑧 ∈ ( 𝑃 ∖ 𝑏 ) ∧ 𝑤 ∈ ( 𝑃 ∖ 𝑏 ) ) ∧ ∃ 𝑡 ∈ 𝑏 𝑡 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) ) )
18	17	cbvopabv	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝑏 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝑏 ) ) ∧ ∃ 𝑠 ∈ 𝑏 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( 𝑃 ∖ 𝑏 ) ∧ 𝑤 ∈ ( 𝑃 ∖ 𝑏 ) ) ∧ ∃ 𝑡 ∈ 𝑏 𝑡 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) }
19		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ↔ 𝑧 ∈ ( 𝑃 ∖ 𝐴 ) ) )
20		eleq1w	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ↔ 𝑤 ∈ ( 𝑃 ∖ 𝐴 ) ) )
21	19 20	bi2anan9	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ↔ ( 𝑧 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑤 ∈ ( 𝑃 ∖ 𝐴 ) ) ) )
22		eleq1w	⊢ ( 𝑠 = 𝑣 → ( 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ 𝑣 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) )
23	22	cbvrexvw	⊢ ( ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑣 ∈ 𝐴 𝑣 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) )
24	13	eleq2d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑣 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ 𝑣 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) )
25	24	rexbidv	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ∃ 𝑣 ∈ 𝐴 𝑣 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑣 ∈ 𝐴 𝑣 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) )
26	23 25	bitrid	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑣 ∈ 𝐴 𝑣 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) )
27	21 26	anbi12d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) ↔ ( ( 𝑧 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑤 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑣 ∈ 𝐴 𝑣 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) ) )
28	27	cbvopabv	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑤 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑣 ∈ 𝐴 𝑣 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) }
29	1 2 3 4 5 6 7 18 28	prlngmolem2	⊢ ( 𝜑 → ∃* 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )