Metamath Proof Explorer

Theorem tglineintmo

Description: Two distinct lines intersect in at most one point. Theorem 6.21 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Hypotheses tglineintmo.p 
|- P = ( Base ` G )
tglineintmo.i 
|- I = ( Itv ` G )
tglineintmo.l 
|- L = ( LineG ` G )
tglineintmo.g 
|- ( ph -> G e. TarskiG )
tglineintmo.a 
|- ( ph -> A e. ran L )
tglineintmo.b 
|- ( ph -> B e. ran L )
tglineintmo.c 
|- ( ph -> A =/= B )
Assertion tglineintmo 
|- ( ph -> E* x ( x e. A /\ x e. B ) )

Proof

Step Hyp Ref Expression
1 tglineintmo.p 
 |-  P = ( Base ` G )
2 tglineintmo.i 
 |-  I = ( Itv ` G )
3 tglineintmo.l 
 |-  L = ( LineG ` G )
4 tglineintmo.g 
 |-  ( ph -> G e. TarskiG )
5 tglineintmo.a 
 |-  ( ph -> A e. ran L )
6 tglineintmo.b 
 |-  ( ph -> B e. ran L )
7 tglineintmo.c 
 |-  ( ph -> A =/= B )
8 4 ad2antrr 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> G e. TarskiG )
9 elssuni 
 |-  ( A e. ran L -> A C_ U. ran L )
10 5 9 syl 
 |-  ( ph -> A C_ U. ran L )
11 1 3 2 tglnunirn 
 |-  ( G e. TarskiG -> U. ran L C_ P )
12 4 11 syl 
 |-  ( ph -> U. ran L C_ P )
13 10 12 sstrd 
 |-  ( ph -> A C_ P )
14 13 ad2antrr 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> A C_ P )
15 simplrl 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> ( x e. A /\ x e. B ) )
16 15 simpld 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> x e. A )
17 14 16 sseldd 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> x e. P )
18 simplrr 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> ( y e. A /\ y e. B ) )
19 18 simpld 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> y e. A )
20 14 19 sseldd 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> y e. P )
21 simpr 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> x =/= y )
22 5 ad2antrr 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> A e. ran L )
23 1 2 3 8 17 20 21 21 22 16 19 tglinethru 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> A = ( x L y ) )
24 6 ad2antrr 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> B e. ran L )
25 15 simprd 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> x e. B )
26 18 simprd 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> y e. B )
27 1 2 3 8 17 20 21 21 24 25 26 tglinethru 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> B = ( x L y ) )
28 23 27 eqtr4d 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> A = B )
29 7 ad2antrr 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> A =/= B )
30 29 neneqd 
 |-  ( ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) /\ x =/= y ) -> -. A = B )
31 28 30 pm2.65da 
 |-  ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) -> -. x =/= y )
32 nne 
 |-  ( -. x =/= y <-> x = y )
33 31 32 sylib 
 |-  ( ( ph /\ ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) ) -> x = y )
34 33 ex 
 |-  ( ph -> ( ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) -> x = y ) )
35 34 alrimivv 
 |-  ( ph -> A. x A. y ( ( ( x e. A /\ x e. B ) /\ ( y e. A /\ y e. B ) ) -> x = y ) )
36 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
37 eleq1w 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
38 36 37 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ x e. B ) <-> ( y e. A /\ y e. B ) ) )
39 38 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 ) )
40 35 39 sylibr 
 |-  ( ph -> E* x ( x e. A /\ x e. B ) )