Step |
Hyp |
Ref |
Expression |
1 |
|
cnvimarndm |
⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹 |
2 |
1
|
a1i |
⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹 ) |
3 |
2
|
difeq1d |
⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( ◡ 𝐹 “ ran 𝐹 ) ∖ ( ◡ 𝐹 “ { 𝑍 } ) ) = ( dom 𝐹 ∖ ( ◡ 𝐹 “ { 𝑍 } ) ) ) |
4 |
|
difpreima |
⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 𝑍 } ) ) = ( ( ◡ 𝐹 “ ran 𝐹 ) ∖ ( ◡ 𝐹 “ { 𝑍 } ) ) ) |
5 |
4
|
3ad2ant1 |
⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 𝑍 } ) ) = ( ( ◡ 𝐹 “ ran 𝐹 ) ∖ ( ◡ 𝐹 “ { 𝑍 } ) ) ) |
6 |
|
suppssdm |
⊢ ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹 |
7 |
|
dfss4 |
⊢ ( ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹 ↔ ( dom 𝐹 ∖ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ( 𝐹 supp 𝑍 ) ) |
8 |
6 7
|
mpbi |
⊢ ( dom 𝐹 ∖ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ( 𝐹 supp 𝑍 ) |
9 |
|
suppiniseg |
⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) = ( ◡ 𝐹 “ { 𝑍 } ) ) |
10 |
9
|
difeq2d |
⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( dom 𝐹 ∖ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ( dom 𝐹 ∖ ( ◡ 𝐹 “ { 𝑍 } ) ) ) |
11 |
8 10
|
eqtr3id |
⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = ( dom 𝐹 ∖ ( ◡ 𝐹 “ { 𝑍 } ) ) ) |
12 |
3 5 11
|
3eqtr4rd |
⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 𝑍 } ) ) ) |