Metamath Proof Explorer

Theorem tgisline

Description: The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Hypotheses tglineelsb2.p 
|- B = ( Base ` G )
tglineelsb2.i 
|- I = ( Itv ` G )
tglineelsb2.l 
|- L = ( LineG ` G )
tglineelsb2.g 
|- ( ph -> G e. TarskiG )
tgisline.1 
|- ( ph -> A e. ran L )
Assertion tgisline 
|- ( ph -> E. x e. B E. y e. B ( A = ( x L y ) /\ x =/= y ) )

Proof

Step Hyp Ref Expression
1 tglineelsb2.p 
 |-  B = ( Base ` G )
2 tglineelsb2.i 
 |-  I = ( Itv ` G )
3 tglineelsb2.l 
 |-  L = ( LineG ` G )
4 tglineelsb2.g 
 |-  ( ph -> G e. TarskiG )
5 tgisline.1 
 |-  ( ph -> A e. ran L )
6 4 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. ( B \ { x } ) ) ) -> G e. TarskiG )
7 simprl 
 |-  ( ( ph /\ ( x e. B /\ y e. ( B \ { x } ) ) ) -> x e. B )
8 simprr 
 |-  ( ( ph /\ ( x e. B /\ y e. ( B \ { x } ) ) ) -> y e. ( B \ { x } ) )
9 8 eldifad 
 |-  ( ( ph /\ ( x e. B /\ y e. ( B \ { x } ) ) ) -> y e. B )
10 eldifsn 
 |-  ( y e. ( B \ { x } ) <-> ( y e. B /\ y =/= x ) )
11 8 10 sylib 
 |-  ( ( ph /\ ( x e. B /\ y e. ( B \ { x } ) ) ) -> ( y e. B /\ y =/= x ) )
12 11 simprd 
 |-  ( ( ph /\ ( x e. B /\ y e. ( B \ { x } ) ) ) -> y =/= x )
13 12 necomd 
 |-  ( ( ph /\ ( x e. B /\ y e. ( B \ { x } ) ) ) -> x =/= y )
14 1 3 2 6 7 9 13 tglngval 
 |-  ( ( ph /\ ( x e. B /\ y e. ( B \ { x } ) ) ) -> ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } )
15 14 13 jca 
 |-  ( ( ph /\ ( x e. B /\ y e. ( B \ { x } ) ) ) -> ( ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } /\ x =/= y ) )
16 15 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. ( B \ { x } ) ( ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } /\ x =/= y ) )
17 1 3 2 tglng 
 |-  ( G e. TarskiG -> L = ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
18 4 17 syl 
 |-  ( ph -> L = ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
19 18 rneqd 
 |-  ( ph -> ran L = ran ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
20 5 19 eleqtrd 
 |-  ( ph -> A e. ran ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
21 eqid 
 |-  ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) = ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } )
22 21 elrnmpog 
 |-  ( A e. ran L -> ( A e. ran ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) <-> E. x e. B E. y e. ( B \ { x } ) A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
23 5 22 syl 
 |-  ( ph -> ( A e. ran ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) <-> E. x e. B E. y e. ( B \ { x } ) A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
24 20 23 mpbid 
 |-  ( ph -> E. x e. B E. y e. ( B \ { x } ) A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } )
25 16 24 r19.29d2r 
 |-  ( ph -> E. x e. B E. y e. ( B \ { x } ) ( ( ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } /\ x =/= y ) /\ A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
26 difss 
 |-  ( B \ { x } ) C_ B
27 simpr 
 |-  ( ( ( ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } /\ x =/= y ) /\ A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) -> A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } )
28 simpll 
 |-  ( ( ( ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } /\ x =/= y ) /\ A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) -> ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } )
29 27 28 eqtr4d 
 |-  ( ( ( ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } /\ x =/= y ) /\ A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) -> A = ( x L y ) )
30 simplr 
 |-  ( ( ( ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } /\ x =/= y ) /\ A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) -> x =/= y )
31 29 30 jca 
 |-  ( ( ( ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } /\ x =/= y ) /\ A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) -> ( A = ( x L y ) /\ x =/= y ) )
32 31 reximi 
 |-  ( E. y e. ( B \ { x } ) ( ( ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } /\ x =/= y ) /\ A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) -> E. y e. ( B \ { x } ) ( A = ( x L y ) /\ x =/= y ) )
33 ssrexv 
 |-  ( ( B \ { x } ) C_ B -> ( E. y e. ( B \ { x } ) ( A = ( x L y ) /\ x =/= y ) -> E. y e. B ( A = ( x L y ) /\ x =/= y ) ) )
34 26 32 33 mpsyl 
 |-  ( E. y e. ( B \ { x } ) ( ( ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } /\ x =/= y ) /\ A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) -> E. y e. B ( A = ( x L y ) /\ x =/= y ) )
35 34 reximi 
 |-  ( E. x e. B E. y e. ( B \ { x } ) ( ( ( x L y ) = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } /\ x =/= y ) /\ A = { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) -> E. x e. B E. y e. B ( A = ( x L y ) /\ x =/= y ) )
36 25 35 syl 
 |-  ( ph -> E. x e. B E. y e. B ( A = ( x L y ) /\ x =/= y ) )