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 = Line 𝒢 ⁡ G
tglng.i ⊢ I = Itv ⁡ G
Assertion tglnfn ⊢ G ∈ 𝒢 Tarski → L Fn P × P ∖ I

Proof

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