Metamath Proof Explorer

Theorem fullfunfnv

Description: The full functional part of F is a function over _V . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fullfunfnv ⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V

Proof

Step Hyp Ref Expression
1 funpartfun ⊢ Fun ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
2 funfn ⊢ Fun ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ↔ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
3 1 2 mpbi ⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
4 0ex ⊢ ∅ ∈ V
5 4 fconst ⊢ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ : V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ⟶ ∅
6 ffn ⊢ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ : V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ⟶ ∅ → V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ Fn V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
7 5 6 ax-mp ⊢ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ Fn V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
8 3 7 pm3.2i ⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∧ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ Fn V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
9 disjdif ⊢ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∩ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = ∅
10 fnun ⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∧ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ Fn V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∧ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∩ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = ∅ → 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ Fn dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
11 8 9 10 mp2an ⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ Fn dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
12 df-fullfun ⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅
13 12 fneq1i ⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V ↔ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ Fn V
14 unvdif ⊢ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = V
15 14 eqcomi ⊢ V = dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
16 15 fneq2i ⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ Fn V ↔ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ Fn dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
17 13 16 bitri ⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V ↔ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × ∅ Fn dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ∪ V ∖ dom ⁡ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
18 11 17 mpbir ⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V