Metamath Proof Explorer

Theorem tglnunirn

Description: Lines are sets of points. (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Hypotheses tglng.p 
|- P = ( Base ` G )
tglng.l 
|- L = ( LineG ` G )
tglng.i 
|- I = ( Itv ` G )
Assertion tglnunirn 
|- ( G e. TarskiG -> U. ran L C_ P )

Proof

Step Hyp Ref Expression
1 tglng.p 
 |-  P = ( Base ` G )
2 tglng.l 
 |-  L = ( LineG ` G )
3 tglng.i 
 |-  I = ( Itv ` G )
4 1 2 3 tglng 
 |-  ( G e. TarskiG -> L = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
5 4 rneqd 
 |-  ( G e. TarskiG -> ran L = ran ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
6 5 eleq2d 
 |-  ( G e. TarskiG -> ( p e. ran L <-> p e. ran ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) ) )
7 6 biimpa 
 |-  ( ( G e. TarskiG /\ p e. ran L ) -> p e. ran ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
8 eqid 
 |-  ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } )
9 1 fvexi 
 |-  P e. _V
10 9 rabex 
 |-  { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } e. _V
11 8 10 elrnmpo 
 |-  ( p e. ran ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) <-> E. x e. P E. y e. ( P \ { x } ) p = { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } )
12 ssrab2 
 |-  { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } C_ P
13 sseq1 
 |-  ( p = { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } -> ( p C_ P <-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } C_ P ) )
14 12 13 mpbiri 
 |-  ( p = { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } -> p C_ P )
15 14 rexlimivw 
 |-  ( E. y e. ( P \ { x } ) p = { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } -> p C_ P )
16 15 rexlimivw 
 |-  ( E. x e. P E. y e. ( P \ { x } ) p = { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } -> p C_ P )
17 11 16 sylbi 
 |-  ( p e. ran ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) -> p C_ P )
18 7 17 syl 
 |-  ( ( G e. TarskiG /\ p e. ran L ) -> p C_ P )
19 18 ralrimiva 
 |-  ( G e. TarskiG -> A. p e. ran L p C_ P )
20 unissb 
 |-  ( U. ran L C_ P <-> A. p e. ran L p C_ P )
21 19 20 sylibr 
 |-  ( G e. TarskiG -> U. ran L C_ P )