Theorem tgplnfn

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

	Ref	Expression
Hypotheses	tgplnfn.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgplnfn.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tgplnfn.i	⊢ 𝐸 = ( hlG ‘ 𝐺 )
	tgplnfn.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
Assertion	tgplnfn	⊢ ( 𝜑 → 𝐸 Fn ( ( ran 𝐿 × 𝑃 ) ∖ ◡ E ) )

Proof

Step	Hyp	Ref	Expression
1		tgplnfn.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgplnfn.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
3		tgplnfn.i	⊢ 𝐸 = ( hlG ‘ 𝐺 )
4		tgplnfn.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5	1	fvexi	⊢ 𝑃 ∈ V
6	5	rabex	⊢ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ∈ V
7	6	rgen2w	⊢ ∀ 𝑎 ∈ ran 𝐿 ∀ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ∈ V
8		eqid	⊢ ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } )
9	8	fmpox	⊢ ( ∀ 𝑎 ∈ ran 𝐿 ∀ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ∈ V ↔ ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) : ∪ 𝑎 ∈ ran 𝐿 ( { 𝑎 } × ( 𝑃 ∖ 𝑎 ) ) ⟶ V )
10	7 9	mpbi	⊢ ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) : ∪ 𝑎 ∈ ran 𝐿 ( { 𝑎 } × ( 𝑃 ∖ 𝑎 ) ) ⟶ V
11		ffn	⊢ ( ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) : ∪ 𝑎 ∈ ran 𝐿 ( { 𝑎 } × ( 𝑃 ∖ 𝑎 ) ) ⟶ V → ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) Fn ∪ 𝑎 ∈ ran 𝐿 ( { 𝑎 } × ( 𝑃 ∖ 𝑎 ) ) )
12	10 11	ax-mp	⊢ ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) Fn ∪ 𝑎 ∈ ran 𝐿 ( { 𝑎 } × ( 𝑃 ∖ 𝑎 ) )
13		xpdifcnvepel	⊢ ∪ 𝑎 ∈ ran 𝐿 ( { 𝑎 } × ( 𝑃 ∖ 𝑎 ) ) = ( ( ran 𝐿 × 𝑃 ) ∖ ◡ E )
14	13	fneq2i	⊢ ( ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) Fn ∪ 𝑎 ∈ ran 𝐿 ( { 𝑎 } × ( 𝑃 ∖ 𝑎 ) ) ↔ ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) Fn ( ( ran 𝐿 × 𝑃 ) ∖ ◡ E ) )
15	12 14	mpbi	⊢ ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) Fn ( ( ran 𝐿 × 𝑃 ) ∖ ◡ E )
16		df-plng	⊢ hlG = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) , 𝑟 ∈ ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } ) )
17		fveq2	⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = ( LineG ‘ 𝐺 ) )
18	17 2	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = 𝐿 )
19	18	rneqd	⊢ ( 𝑔 = 𝐺 → ran ( LineG ‘ 𝑔 ) = ran 𝐿 )
20		fveq2	⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
21	20 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
22	21	difeq1d	⊢ ( 𝑔 = 𝐺 → ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) = ( 𝑃 ∖ 𝑎 ) )
23		biidd	⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ 𝑎 ↔ 𝑥 ∈ 𝑎 ) )
24		fveq2	⊢ ( 𝑔 = 𝐺 → ( hpG ‘ 𝑔 ) = ( hpG ‘ 𝐺 ) )
25	24	fveq1d	⊢ ( 𝑔 = 𝐺 → ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) = ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) )
26	25	breqd	⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ↔ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ) )
27		fveq2	⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = ( Itv ‘ 𝐺 ) )
28	27	oveqd	⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) = ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) )
29	28	eleq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ↔ 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) )
30	29	rexbidv	⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ↔ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) )
31	23 26 30	3orbi123d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) ↔ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) ) )
32	21 31	rabeqbidv	⊢ ( 𝑔 = 𝐺 → { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } )
33	19 22 32	mpoeq123dv	⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) , 𝑟 ∈ ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } ) = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) )
34	4	elexd	⊢ ( 𝜑 → 𝐺 ∈ V )
35	2	fvexi	⊢ 𝐿 ∈ V
36	35	rnex	⊢ ran 𝐿 ∈ V
37	36	a1i	⊢ ( 𝜑 → ran 𝐿 ∈ V )
38	5	difexi	⊢ ( 𝑃 ∖ 𝑎 ) ∈ V
39	38	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) → ( 𝑃 ∖ 𝑎 ) ∈ V )
40	37 39	mpoexd	⊢ ( 𝜑 → ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) ∈ V )
41	16 33 34 40	fvmptd3	⊢ ( 𝜑 → ( hlG ‘ 𝐺 ) = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) )
42	3 41	eqtrid	⊢ ( 𝜑 → 𝐸 = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) )
43	42	fneq1d	⊢ ( 𝜑 → ( 𝐸 Fn ( ( ran 𝐿 × 𝑃 ) ∖ ◡ E ) ↔ ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑟 ) ) } ) Fn ( ( ran 𝐿 × 𝑃 ) ∖ ◡ E ) ) )
44	15 43	mpbiri	⊢ ( 𝜑 → 𝐸 Fn ( ( ran 𝐿 × 𝑃 ) ∖ ◡ E ) )