Metamath Proof Explorer

Theorem tgplnfn

Description: The plane generating function as a function. (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses tgplnfn.p 
|- P = ( Base ` G )
tgplnfn.l 
|- L = ( LineG ` G )
tgplnfn.i 
|- E = ( PlnG ` G )
tgplnfn.1 
|- ( ph -> G e. V )
Assertion tgplnfn 
|- ( ph -> E Fn ( ( ran L X. P ) \ `' _E ) )

Proof

Step Hyp Ref Expression
1 tgplnfn.p 
 |-  P = ( Base ` G )
2 tgplnfn.l 
 |-  L = ( LineG ` G )
3 tgplnfn.i 
 |-  E = ( PlnG ` G )
4 tgplnfn.1 
 |-  ( ph -> G e. V )
5 1 fvexi 
 |-  P e. _V
6 5 rabex 
 |-  { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } e. _V
7 6 rgen2w 
 |-  A. a e. ran L A. r e. ( P \ a ) { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } e. _V
8 eqid 
 |-  ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) = ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } )
9 8 fmpox 
 |-  ( A. a e. ran L A. r e. ( P \ a ) { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } e. _V <-> ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) : U_ a e. ran L ( { a } X. ( P \ a ) ) --> _V )
10 7 9 mpbi 
 |-  ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) : U_ a e. ran L ( { a } X. ( P \ a ) ) --> _V
11 ffn 
 |-  ( ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) : U_ a e. ran L ( { a } X. ( P \ a ) ) --> _V -> ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) Fn U_ a e. ran L ( { a } X. ( P \ a ) ) )
12 10 11 ax-mp 
 |-  ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) Fn U_ a e. ran L ( { a } X. ( P \ a ) )
13 xpdifcnvepel 
 |-  U_ a e. ran L ( { a } X. ( P \ a ) ) = ( ( ran L X. P ) \ `' _E )
14 13 fneq2i 
 |-  ( ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) Fn U_ a e. ran L ( { a } X. ( P \ a ) ) <-> ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) Fn ( ( ran L X. P ) \ `' _E ) )
15 12 14 mpbi 
 |-  ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) Fn ( ( ran L X. P ) \ `' _E )
16 df-plng 
 |-  PlnG = ( g e. _V |-> ( a e. ran ( LineG ` g ) , r e. ( ( Base ` g ) \ a ) |-> { x e. ( Base ` g ) | ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) } ) )
17 fveq2 
 |-  ( g = G -> ( LineG ` g ) = ( LineG ` G ) )
18 17 2 eqtr4di 
 |-  ( g = G -> ( LineG ` g ) = L )
19 18 rneqd 
 |-  ( g = G -> ran ( LineG ` g ) = ran L )
20 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
21 20 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
22 21 difeq1d 
 |-  ( g = G -> ( ( Base ` g ) \ a ) = ( P \ a ) )
23 biidd 
 |-  ( g = G -> ( x e. a <-> x e. a ) )
24 fveq2 
 |-  ( g = G -> ( hpG ` g ) = ( hpG ` G ) )
25 24 fveq1d 
 |-  ( g = G -> ( ( hpG ` g ) ` a ) = ( ( hpG ` G ) ` a ) )
26 25 breqd 
 |-  ( g = G -> ( x ( ( hpG ` g ) ` a ) r <-> x ( ( hpG ` G ) ` a ) r ) )
27 fveq2 
 |-  ( g = G -> ( Itv ` g ) = ( Itv ` G ) )
28 27 oveqd 
 |-  ( g = G -> ( x ( Itv ` g ) r ) = ( x ( Itv ` G ) r ) )
29 28 eleq2d 
 |-  ( g = G -> ( t e. ( x ( Itv ` g ) r ) <-> t e. ( x ( Itv ` G ) r ) ) )
30 29 rexbidv 
 |-  ( g = G -> ( E. t e. a t e. ( x ( Itv ` g ) r ) <-> E. t e. a t e. ( x ( Itv ` G ) r ) ) )
31 23 26 30 3orbi123d 
 |-  ( g = G -> ( ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) <-> ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) ) )
32 21 31 rabeqbidv 
 |-  ( g = G -> { x e. ( Base ` g ) | ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) } = { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } )
33 19 22 32 mpoeq123dv 
 |-  ( g = G -> ( a e. ran ( LineG ` g ) , r e. ( ( Base ` g ) \ a ) |-> { x e. ( Base ` g ) | ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) } ) = ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) )
34 4 elexd 
 |-  ( ph -> G e. _V )
35 2 fvexi 
 |-  L e. _V
36 35 rnex 
 |-  ran L e. _V
37 36 a1i 
 |-  ( ph -> ran L e. _V )
38 5 difexi 
 |-  ( P \ a ) e. _V
39 38 a1i 
 |-  ( ( ph /\ a e. ran L ) -> ( P \ a ) e. _V )
40 37 39 mpoexd 
 |-  ( ph -> ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) e. _V )
41 16 33 34 40 fvmptd3 
 |-  ( ph -> ( PlnG ` G ) = ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) )
42 3 41 eqtrid 
 |-  ( ph -> E = ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) )
43 42 fneq1d 
 |-  ( ph -> ( E Fn ( ( ran L X. P ) \ `' _E ) <-> ( a e. ran L , r e. ( P \ a ) |-> { x e. P | ( x e. a \/ x ( ( hpG ` G ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` G ) r ) ) } ) Fn ( ( ran L X. P ) \ `' _E ) ) )
44 15 43 mpbiri 
 |-  ( ph -> E Fn ( ( ran L X. P ) \ `' _E ) )