Theorem perpin

Description: If two lines A and B are perpendicular, then they intersect. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	perpin.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	perpin.2	⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
Assertion	perpin	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		perpin.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
2		perpin.2	⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
3		ne0i	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
4	3	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
5		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
7		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
8		eqid	⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
9	8 1 2	perpln1	⊢ ( 𝜑 → 𝐴 ∈ ran ( LineG ‘ 𝐺 ) )
10	8 1 2	perpln2	⊢ ( 𝜑 → 𝐵 ∈ ran ( LineG ‘ 𝐺 ) )
11	5 6 7 8 1 9 10	isperp	⊢ ( 𝜑 → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
12	2 11	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
13	4 12	r19.29a	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )