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 = Line 𝒢 ⁡ G
tgplnfn.i No typesetting found for |- E = ( PlnG ` G ) with typecode |-
tgplnfn.1 ⊢ φ → G ∈ V
Assertion tgplnfn ⊢ φ → E Fn ran ⁡ L × P ∖ E -1

Proof

Step Hyp Ref Expression
1 tgplnfn.p ⊢ P = Base G
2 tgplnfn.l ⊢ L = Line 𝒢 ⁡ G
3 tgplnfn.i Could not format E = ( PlnG ` G ) : No typesetting found for |- E = ( PlnG ` G ) with typecode |-
4 tgplnfn.1 ⊢ φ → G ∈ V
5 1 fvexi ⊢ P ∈ V
6 5 rabex ⊢ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r ∈ V
7 6 rgen2w ⊢ ∀ a ∈ ran ⁡ L ∀ r ∈ P ∖ a x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r ∈ V
8 eqid ⊢ a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r = a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r
9 8 fmpox ⊢ ∀ a ∈ ran ⁡ L ∀ r ∈ P ∖ a x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r ∈ V ↔ a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r : ⋃ a ∈ ran ⁡ L a × P ∖ a ⟶ V
10 7 9 mpbi ⊢ a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r : ⋃ a ∈ ran ⁡ L a × P ∖ a ⟶ V
11 ffn ⊢ a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r : ⋃ a ∈ ran ⁡ L a × P ∖ a ⟶ V → a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r Fn ⋃ a ∈ ran ⁡ L a × P ∖ a
12 10 11 ax-mp ⊢ a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r Fn ⋃ a ∈ ran ⁡ L a × P ∖ a
13 xpdifcnvepel ⊢ ⋃ a ∈ ran ⁡ L a × P ∖ a = ran ⁡ L × P ∖ E -1
14 13 fneq2i ⊢ a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r Fn ⋃ a ∈ ran ⁡ L a × P ∖ a ↔ a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r Fn ran ⁡ L × P ∖ E -1
15 12 14 mpbi ⊢ a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r Fn ran ⁡ L × P ∖ E -1
16 df-plng Could not format 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 ) ) } ) ) : No typesetting found for |- 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 ) ) } ) ) with typecode |-
17 fveq2 ⊢ g = G → Line 𝒢 ⁡ g = Line 𝒢 ⁡ G
18 17 2 eqtr4di ⊢ g = G → Line 𝒢 ⁡ g = L
19 18 rneqd ⊢ g = G → ran ⁡ Line 𝒢 ⁡ 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 ∈ a ↔ x ∈ a
24 fveq2 ⊢ g = G → hp 𝒢 ⁡ g = hp 𝒢 ⁡ G
25 24 fveq1d ⊢ g = G → hp 𝒢 ⁡ g ⁡ a = hp 𝒢 ⁡ G ⁡ a
26 25 breqd ⊢ g = G → x hp 𝒢 ⁡ g ⁡ a r ↔ x hp 𝒢 ⁡ 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 ∈ x Itv ⁡ g r ↔ t ∈ x Itv ⁡ G r
30 29 rexbidv ⊢ g = G → ∃ t ∈ a t ∈ x Itv ⁡ g r ↔ ∃ t ∈ a t ∈ x Itv ⁡ G r
31 23 26 30 3orbi123d ⊢ g = G → x ∈ a ∨ x hp 𝒢 ⁡ g ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ g r ↔ x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r
32 21 31 rabeqbidv ⊢ g = G → x ∈ Base g | x ∈ a ∨ x hp 𝒢 ⁡ g ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ g r = x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r
33 19 22 32 mpoeq123dv ⊢ g = G → a ∈ ran ⁡ Line 𝒢 ⁡ g , r ∈ Base g ∖ a ⟼ x ∈ Base g | x ∈ a ∨ x hp 𝒢 ⁡ g ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ g r = a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r
34 4 elexd ⊢ φ → G ∈ V
35 2 fvexi ⊢ L ∈ V
36 35 rnex ⊢ ran ⁡ L ∈ V
37 36 a1i ⊢ φ → ran ⁡ L ∈ V
38 5 difexi ⊢ P ∖ a ∈ V
39 38 a1i ⊢ φ ∧ a ∈ ran ⁡ L → P ∖ a ∈ V
40 37 39 mpoexd ⊢ φ → a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r ∈ V
41 16 33 34 40 fvmptd3 Could not format ( 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 ) ) } ) ) : No typesetting found for |- ( 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 ) ) } ) ) with typecode |-
42 3 41 eqtrid ⊢ φ → E = a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r
43 42 fneq1d ⊢ φ → E Fn ran ⁡ L × P ∖ E -1 ↔ a ∈ ran ⁡ L , r ∈ P ∖ a ⟼ x ∈ P | x ∈ a ∨ x hp 𝒢 ⁡ G ⁡ a r ∨ ∃ t ∈ a t ∈ x Itv ⁡ G r Fn ran ⁡ L × P ∖ E -1
44 15 43 mpbiri ⊢ φ → E Fn ran ⁡ L × P ∖ E -1