Metamath Proof Explorer

Theorem suppcofnd

Description: The support of the composition of two functions. (Contributed by SN, 15-Sep-2023)

Ref Expression
Hypotheses suppcofnd.z ⊢ φ → Z ∈ U
suppcofnd.f ⊢ φ → F Fn A
suppcofnd.a ⊢ φ → A ∈ V
suppcofnd.g ⊢ φ → G Fn B
suppcofnd.b ⊢ φ → B ∈ W
Assertion suppcofnd ⊢ φ → F ∘ G supp Z = x ∈ B | G ⁡ x ∈ A ∧ F ⁡ G ⁡ x ≠ Z

Proof

Step Hyp Ref Expression
1 suppcofnd.z ⊢ φ → Z ∈ U
2 suppcofnd.f ⊢ φ → F Fn A
3 suppcofnd.a ⊢ φ → A ∈ V
4 suppcofnd.g ⊢ φ → G Fn B
5 suppcofnd.b ⊢ φ → B ∈ W
6 2 3 fnexd ⊢ φ → F ∈ V
7 4 5 fnexd ⊢ φ → G ∈ V
8 suppco ⊢ F ∈ V ∧ G ∈ V → F ∘ G supp Z = G -1 F supp Z
9 6 7 8 syl2anc ⊢ φ → F ∘ G supp Z = G -1 F supp Z
10 fncnvima2 ⊢ G Fn B → G -1 F supp Z = x ∈ B | G ⁡ x ∈ supp Z⁡ F
11 4 10 syl ⊢ φ → G -1 F supp Z = x ∈ B | G ⁡ x ∈ supp Z⁡ F
12 elsuppfn ⊢ F Fn A ∧ A ∈ V ∧ Z ∈ U → G ⁡ x ∈ supp Z⁡ F ↔ G ⁡ x ∈ A ∧ F ⁡ G ⁡ x ≠ Z
13 2 3 1 12 syl3anc ⊢ φ → G ⁡ x ∈ supp Z⁡ F ↔ G ⁡ x ∈ A ∧ F ⁡ G ⁡ x ≠ Z
14 13 rabbidv ⊢ φ → x ∈ B | G ⁡ x ∈ supp Z⁡ F = x ∈ B | G ⁡ x ∈ A ∧ F ⁡ G ⁡ x ≠ Z
15 9 11 14 3eqtrd ⊢ φ → F ∘ G supp Z = x ∈ B | G ⁡ x ∈ A ∧ F ⁡ G ⁡ x ≠ Z