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 
|- ( ( A e. LinesEE /\ B e. LinesEE /\ A =/= B ) -> E* x ( x e. A /\ x e. B ) )

Proof

Step Hyp Ref Expression
1 an4 
 |-  ( ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) <-> ( ( x e. A /\ y e. A ) /\ ( x e. B /\ y e. B ) ) )
2 linethru 
 |-  ( ( A e. LinesEE /\ ( x e. A /\ y e. A ) /\ x =/= y ) -> A = ( x Line y ) )
3 2 3expa 
 |-  ( ( ( A e. LinesEE /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) -> A = ( x Line y ) )
4 linethru 
 |-  ( ( B e. LinesEE /\ ( x e. B /\ y e. B ) /\ x =/= y ) -> B = ( x Line y ) )
5 4 3expa 
 |-  ( ( ( B e. LinesEE /\ ( x e. B /\ y e. B ) ) /\ x =/= y ) -> B = ( x Line y ) )
6 eqtr3 
 |-  ( ( A = ( x Line y ) /\ B = ( x Line y ) ) -> A = B )
7 3 5 6 syl2an 
 |-  ( ( ( ( A e. LinesEE /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) /\ ( ( B e. LinesEE /\ ( x e. B /\ y e. B ) ) /\ x =/= y ) ) -> A = B )
8 7 anandirs 
 |-  ( ( ( ( A e. LinesEE /\ ( x e. A /\ y e. A ) ) /\ ( B e. LinesEE /\ ( x e. B /\ y e. B ) ) ) /\ x =/= y ) -> A = B )
9 8 ex 
 |-  ( ( ( A e. LinesEE /\ ( x e. A /\ y e. A ) ) /\ ( B e. LinesEE /\ ( x e. B /\ y e. B ) ) ) -> ( x =/= y -> A = B ) )
10 9 necon1d 
 |-  ( ( ( A e. LinesEE /\ ( x e. A /\ y e. A ) ) /\ ( B e. LinesEE /\ ( x e. B /\ y e. B ) ) ) -> ( A =/= B -> x = y ) )
11 10 an4s 
 |-  ( ( ( A e. LinesEE /\ B e. LinesEE ) /\ ( ( x e. A /\ y e. A ) /\ ( x e. B /\ y e. B ) ) ) -> ( A =/= B -> x = y ) )
12 1 11 sylan2b 
 |-  ( ( ( A e. LinesEE /\ B e. LinesEE ) /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) -> ( A =/= B -> x = y ) )
13 12 ex 
 |-  ( ( A e. LinesEE /\ B e. LinesEE ) -> ( ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) -> ( A =/= B -> x = y ) ) )
14 13 com23 
 |-  ( ( A e. LinesEE /\ B e. LinesEE ) -> ( A =/= B -> ( ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) -> x = y ) ) )
15 14 3impia 
 |-  ( ( A e. LinesEE /\ B e. LinesEE /\ A =/= B ) -> ( ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) -> x = y ) )
16 15 alrimivv 
 |-  ( ( A e. LinesEE /\ B e. LinesEE /\ A =/= B ) -> A. x A. y ( ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) -> x = y ) )
17 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
18 eleq1w 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
19 17 18 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ x e. B ) <-> ( y e. A /\ y e. B ) ) )
20 19 mo4 
 |-  ( E* x ( x e. A /\ x e. B ) <-> A. x A. y ( ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) -> x = y ) )
21 16 20 sylibr 
 |-  ( ( A e. LinesEE /\ B e. LinesEE /\ A =/= B ) -> E* x ( x e. A /\ x e. B ) )