Metamath Proof Explorer

Theorem tglnfn

Description: Lines as functions. (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Hypotheses tglng.p ⊢P=BaseG
tglng.l ⊢L=Line𝒢⁡G
tglng.i ⊢I=Itv⁡G
Assertion tglnfn ⊢G∈𝒢Tarski→LFnP×P∖I

Proof

Step Hyp Ref Expression
1 tglng.p ⊢P=BaseG
2 tglng.l ⊢L=Line𝒢⁡G
3 tglng.i ⊢I=Itv⁡G
4 1 fvexi ⊢P∈V
5 4 rabex ⊢z∈P|z∈xIy∨x∈zIy∨y∈xIz∈V
6 5 rgen2w ⊢∀x∈P∀y∈P∖xz∈P|z∈xIy∨x∈zIy∨y∈xIz∈V
7 eqid ⊢x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
8 7 fmpox ⊢∀x∈P∀y∈P∖xz∈P|z∈xIy∨x∈zIy∨y∈xIz∈V↔x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz:⋃x∈Px×P∖x⟶V
9 6 8 mpbi ⊢x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz:⋃x∈Px×P∖x⟶V
10 ffn ⊢x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz:⋃x∈Px×P∖x⟶V→x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIzFn⋃x∈Px×P∖x
11 9 10 ax-mp ⊢x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIzFn⋃x∈Px×P∖x
12 xpdifid ⊢⋃x∈Px×P∖x=P×P∖I
13 12 fneq2i ⊢x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIzFn⋃x∈Px×P∖x↔x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIzFnP×P∖I
14 11 13 mpbi ⊢x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIzFnP×P∖I
15 1 2 3 tglng ⊢G∈𝒢Tarski→L=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
16 15 fneq1d ⊢G∈𝒢Tarski→LFnP×P∖I↔x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIzFnP×P∖I
17 14 16 mpbiri ⊢G∈𝒢Tarski→LFnP×P∖I