Metamath Proof Explorer

Theorem lineintmo

Description: Two distinct lines intersect in at most one point. Theorem 6.21 of Schwabhauser p. 46. (Contributed by Scott Fenton, 29-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion lineintmo ( ( 𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ∧ 𝐴 ≠ 𝐵 ) → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 an4 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
2 linethru ⊢ ( ( 𝐴 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 = ( 𝑥 Line 𝑦 ) )
3 2 3expa ⊢ ( ( ( 𝐴 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 = ( 𝑥 Line 𝑦 ) )
4 linethru ⊢ ( ( 𝐵 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑦 ) → 𝐵 = ( 𝑥 Line 𝑦 ) )
5 4 3expa ⊢ ( ( ( 𝐵 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐵 = ( 𝑥 Line 𝑦 ) )
6 eqtr3 ⊢ ( ( 𝐴 = ( 𝑥 Line 𝑦 ) ∧ 𝐵 = ( 𝑥 Line 𝑦 ) ) → 𝐴 = 𝐵 )
7 3 5 6 syl2an ⊢ ( ( ( ( 𝐴 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( ( 𝐵 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐴 = 𝐵 )
8 7 anandirs ⊢ ( ( ( ( 𝐴 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐵 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝐴 = 𝐵 )
9 8 ex ⊢ ( ( ( 𝐴 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐵 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝑥 ≠ 𝑦 → 𝐴 = 𝐵 ) )
10 9 necon1d ⊢ ( ( ( 𝐴 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐵 ∈ LinesEE ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝐴 ≠ 𝐵 → 𝑥 = 𝑦 ) )
11 10 an4s ⊢ ( ( ( 𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝐴 ≠ 𝐵 → 𝑥 = 𝑦 ) )
12 1 11 sylan2b ⊢ ( ( ( 𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( 𝐴 ≠ 𝐵 → 𝑥 = 𝑦 ) )
13 12 ex ⊢ ( ( 𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ≠ 𝐵 → 𝑥 = 𝑦 ) ) )
14 13 com23 ⊢ ( ( 𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ) → ( 𝐴 ≠ 𝐵 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 = 𝑦 ) ) )
15 14 3impia ⊢ ( ( 𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 = 𝑦 ) )
16 15 alrimivv ⊢ ( ( 𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 = 𝑦 ) )
17 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
18 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
19 17 18 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
20 19 mo4 ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 = 𝑦 ) )
21 16 20 sylibr ⊢ ( ( 𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ∧ 𝐴 ≠ 𝐵 ) → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )