Metamath Proof Explorer

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 ⊢ φ → G ∈ 𝒢 Tarski
perpin.2 ⊢ φ → A ⟂ 𝒢 ⁡ G B
Assertion perpin ⊢ φ → A ∩ B ≠ ∅

Proof

Step Hyp Ref Expression
1 perpin.1 ⊢ φ → G ∈ 𝒢 Tarski
2 perpin.2 ⊢ φ → A ⟂ 𝒢 ⁡ G B
3 ne0i ⊢ x ∈ A ∩ B → A ∩ B ≠ ∅
4 3 ad2antlr ⊢ φ ∧ x ∈ A ∩ B ∧ ∀ u ∈ A ∀ v ∈ B ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ G → A ∩ B ≠ ∅
5 eqid ⊢ Base G = Base G
6 eqid ⊢ dist ⁡ G = dist ⁡ G
7 eqid ⊢ Itv ⁡ G = Itv ⁡ G
8 eqid ⊢ Line 𝒢 ⁡ G = Line 𝒢 ⁡ G
9 8 1 2 perpln1 ⊢ φ → A ∈ ran ⁡ Line 𝒢 ⁡ G
10 8 1 2 perpln2 ⊢ φ → B ∈ ran ⁡ Line 𝒢 ⁡ G
11 5 6 7 8 1 9 10 isperp ⊢ φ → A ⟂ 𝒢 ⁡ G B ↔ ∃ x ∈ A ∩ B ∀ u ∈ A ∀ v ∈ B ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ G
12 2 11 mpbid ⊢ φ → ∃ x ∈ A ∩ B ∀ u ∈ A ∀ v ∈ B ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ G
13 4 12 r19.29a ⊢ φ → A ∩ B ≠ ∅