This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem suppvalfn

Description: The value of the operation constructing the support of a function with a given domain. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 22-Apr-2019)

Ref Expression
Assertion suppvalfn ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → F supp Z = i ∈ X | F ⁡ i ≠ Z

Proof

Step Hyp Ref Expression
1 fnfun ⊢ F Fn X → Fun ⁡ F
2 1 3ad2ant1 ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → Fun ⁡ F
3 fnex ⊢ F Fn X ∧ X ∈ V → F ∈ V
4 3 3adant3 ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → F ∈ V
5 simp3 ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → Z ∈ W
6 suppval1 ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F supp Z = i ∈ dom ⁡ F | F ⁡ i ≠ Z
7 2 4 5 6 syl3anc ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → F supp Z = i ∈ dom ⁡ F | F ⁡ i ≠ Z
8 fndm ⊢ F Fn X → dom ⁡ F = X
9 8 3ad2ant1 ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → dom ⁡ F = X
10 9 rabeqdv ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → i ∈ dom ⁡ F | F ⁡ i ≠ Z = i ∈ X | F ⁡ i ≠ Z
11 7 10 eqtrd ⊢ F Fn X ∧ X ∈ V ∧ Z ∈ W → F supp Z = i ∈ X | F ⁡ i ≠ Z