Description: The support of a function in maps-to notation with a class difference. (Contributed by AV, 28-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mptsuppdifd.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) | |
mptsuppdifd.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | ||
mptsuppdifd.z | ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 ) | ||
Assertion | mptsuppdifd | ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( V ∖ { 𝑍 } ) } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mptsuppdifd.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) | |
2 | mptsuppdifd.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | |
3 | mptsuppdifd.z | ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 ) | |
4 | 2 | mptexd | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) |
5 | 1 4 | eqeltrid | ⊢ ( 𝜑 → 𝐹 ∈ V ) |
6 | suppimacnv | ⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) | |
7 | 5 3 6 | syl2anc | ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) |
8 | 1 | mptpreima | ⊢ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( V ∖ { 𝑍 } ) } |
9 | 7 8 | eqtrdi | ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( V ∖ { 𝑍 } ) } ) |