Metamath Proof Explorer

Theorem frnsuppeq

Description: Two ways of writing the support of a function with known codomain. (Contributed by Stefan O'Rear, 9-Jul-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Assertion frnsuppeq ⊢ I ∈ V ∧ Z ∈ W → F : I ⟶ S → F supp Z = F -1 S ∖ Z

Proof

Step Hyp Ref Expression
1 fex ⊢ F : I ⟶ S ∧ I ∈ V → F ∈ V
2 1 expcom ⊢ I ∈ V → F : I ⟶ S → F ∈ V
3 2 adantr ⊢ I ∈ V ∧ Z ∈ W → F : I ⟶ S → F ∈ V
4 3 imp ⊢ I ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → F ∈ V
5 simplr ⊢ I ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → Z ∈ W
6 suppimacnv ⊢ F ∈ V ∧ Z ∈ W → F supp Z = F -1 V ∖ Z
7 4 5 6 syl2anc ⊢ I ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → F supp Z = F -1 V ∖ Z
8 ffun ⊢ F : I ⟶ S → Fun ⁡ F
9 inpreima ⊢ Fun ⁡ F → F -1 S ∩ V ∖ Z = F -1 S ∩ F -1 V ∖ Z
10 8 9 syl ⊢ F : I ⟶ S → F -1 S ∩ V ∖ Z = F -1 S ∩ F -1 V ∖ Z
11 cnvimass ⊢ F -1 V ∖ Z ⊆ dom ⁡ F
12 fdm ⊢ F : I ⟶ S → dom ⁡ F = I
13 fimacnv ⊢ F : I ⟶ S → F -1 S = I
14 12 13 eqtr4d ⊢ F : I ⟶ S → dom ⁡ F = F -1 S
15 11 14 sseqtrid ⊢ F : I ⟶ S → F -1 V ∖ Z ⊆ F -1 S
16 sseqin2 ⊢ F -1 V ∖ Z ⊆ F -1 S ↔ F -1 S ∩ F -1 V ∖ Z = F -1 V ∖ Z
17 15 16 sylib ⊢ F : I ⟶ S → F -1 S ∩ F -1 V ∖ Z = F -1 V ∖ Z
18 10 17 eqtrd ⊢ F : I ⟶ S → F -1 S ∩ V ∖ Z = F -1 V ∖ Z
19 invdif ⊢ S ∩ V ∖ Z = S ∖ Z
20 19 imaeq2i ⊢ F -1 S ∩ V ∖ Z = F -1 S ∖ Z
21 18 20 eqtr3di ⊢ F : I ⟶ S → F -1 V ∖ Z = F -1 S ∖ Z
22 21 adantl ⊢ I ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → F -1 V ∖ Z = F -1 S ∖ Z
23 7 22 eqtrd ⊢ I ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → F supp Z = F -1 S ∖ Z
24 23 ex ⊢ I ∈ V ∧ Z ∈ W → F : I ⟶ S → F supp Z = F -1 S ∖ Z