Metamath Proof Explorer

Theorem frnsuppeqg

Description: Version of frnsuppeq avoiding ax-rep by assuming F is a set rather than its domain I . (Contributed by SN, 30-Jul-2024)

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

Proof

Step Hyp Ref Expression
1 suppimacnv ⊢ F ∈ V ∧ Z ∈ W → F supp Z = F -1 V ∖ Z
2 invdif ⊢ S ∩ V ∖ Z = S ∖ Z
3 2 imaeq2i ⊢ F -1 S ∩ V ∖ Z = F -1 S ∖ Z
4 ffun ⊢ F : I ⟶ S → Fun ⁡ F
5 inpreima ⊢ Fun ⁡ F → F -1 S ∩ V ∖ Z = F -1 S ∩ F -1 V ∖ Z
6 4 5 syl ⊢ F : I ⟶ S → F -1 S ∩ V ∖ Z = F -1 S ∩ F -1 V ∖ Z
7 cnvimass ⊢ F -1 V ∖ Z ⊆ dom ⁡ F
8 fdm ⊢ F : I ⟶ S → dom ⁡ F = I
9 fimacnv ⊢ F : I ⟶ S → F -1 S = I
10 8 9 eqtr4d ⊢ F : I ⟶ S → dom ⁡ F = F -1 S
11 7 10 sseqtrid ⊢ F : I ⟶ S → F -1 V ∖ Z ⊆ F -1 S
12 sseqin2 ⊢ F -1 V ∖ Z ⊆ F -1 S ↔ F -1 S ∩ F -1 V ∖ Z = F -1 V ∖ Z
13 11 12 sylib ⊢ F : I ⟶ S → F -1 S ∩ F -1 V ∖ Z = F -1 V ∖ Z
14 6 13 eqtrd ⊢ F : I ⟶ S → F -1 S ∩ V ∖ Z = F -1 V ∖ Z
15 3 14 syl5reqr ⊢ F : I ⟶ S → F -1 V ∖ Z = F -1 S ∖ Z
16 1 15 sylan9eq ⊢ F ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → F supp Z = F -1 S ∖ Z
17 16 ex ⊢ F ∈ V ∧ Z ∈ W → F : I ⟶ S → F supp Z = F -1 S ∖ Z