Metamath Proof Explorer

Theorem tglnfn

Description: Lines as functions. (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 tglnfn 
|- ( G e. TarskiG -> L Fn ( ( P X. P ) \ _I ) )

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 fvexi 
 |-  P e. _V
5 4 rabex 
 |-  { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } e. _V
6 5 rgen2w 
 |-  A. x e. P A. y e. ( P \ { x } ) { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } e. _V
7 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 ) ) } )
8 7 fmpox 
 |-  ( A. x e. P A. y e. ( P \ { x } ) { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } e. _V <-> ( 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 ) ) } ) : U_ x e. P ( { x } X. ( P \ { x } ) ) --> _V )
9 6 8 mpbi 
 |-  ( 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 ) ) } ) : U_ x e. P ( { x } X. ( P \ { x } ) ) --> _V
10 ffn 
 |-  ( ( 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 ) ) } ) : U_ x e. P ( { x } X. ( P \ { x } ) ) --> _V -> ( 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 ) ) } ) Fn U_ x e. P ( { x } X. ( P \ { x } ) ) )
11 9 10 ax-mp 
 |-  ( 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 ) ) } ) Fn U_ x e. P ( { x } X. ( P \ { x } ) )
12 xpdifid 
 |-  U_ x e. P ( { x } X. ( P \ { x } ) ) = ( ( P X. P ) \ _I )
13 12 fneq2i 
 |-  ( ( 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 ) ) } ) Fn U_ x e. P ( { x } X. ( P \ { x } ) ) <-> ( 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 ) ) } ) Fn ( ( P X. P ) \ _I ) )
14 11 13 mpbi 
 |-  ( 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 ) ) } ) Fn ( ( P X. P ) \ _I )
15 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 ) ) } ) )
16 15 fneq1d 
 |-  ( G e. TarskiG -> ( L Fn ( ( P X. P ) \ _I ) <-> ( 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 ) ) } ) Fn ( ( P X. P ) \ _I ) ) )
17 14 16 mpbiri 
 |-  ( G e. TarskiG -> L Fn ( ( P X. P ) \ _I ) )