Step |
Hyp |
Ref |
Expression |
1 |
|
fex |
⊢ ( ( 𝐹 : 𝐼 ⟶ 𝑆 ∧ 𝐼 ∈ 𝑉 ) → 𝐹 ∈ V ) |
2 |
1
|
expcom |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 : 𝐼 ⟶ 𝑆 → 𝐹 ∈ V ) ) |
3 |
2
|
adantr |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → 𝐹 ∈ V ) ) |
4 |
3
|
imp |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → 𝐹 ∈ V ) |
5 |
|
simplr |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → 𝑍 ∈ 𝑊 ) |
6 |
|
suppimacnv |
⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) |
7 |
4 5 6
|
syl2anc |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) |
8 |
|
ffun |
⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → Fun 𝐹 ) |
9 |
|
inpreima |
⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝑆 ∩ ( V ∖ { 𝑍 } ) ) ) = ( ( ◡ 𝐹 “ 𝑆 ) ∩ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ) |
10 |
8 9
|
syl |
⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ◡ 𝐹 “ ( 𝑆 ∩ ( V ∖ { 𝑍 } ) ) ) = ( ( ◡ 𝐹 “ 𝑆 ) ∩ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ) |
11 |
|
cnvimass |
⊢ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ dom 𝐹 |
12 |
|
fdm |
⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → dom 𝐹 = 𝐼 ) |
13 |
|
fimacnv |
⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ◡ 𝐹 “ 𝑆 ) = 𝐼 ) |
14 |
12 13
|
eqtr4d |
⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → dom 𝐹 = ( ◡ 𝐹 “ 𝑆 ) ) |
15 |
11 14
|
sseqtrid |
⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ ( ◡ 𝐹 “ 𝑆 ) ) |
16 |
|
sseqin2 |
⊢ ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ ( ◡ 𝐹 “ 𝑆 ) ↔ ( ( ◡ 𝐹 “ 𝑆 ) ∩ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) |
17 |
15 16
|
sylib |
⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ( ◡ 𝐹 “ 𝑆 ) ∩ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) |
18 |
10 17
|
eqtrd |
⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ◡ 𝐹 “ ( 𝑆 ∩ ( V ∖ { 𝑍 } ) ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) |
19 |
|
invdif |
⊢ ( 𝑆 ∩ ( V ∖ { 𝑍 } ) ) = ( 𝑆 ∖ { 𝑍 } ) |
20 |
19
|
imaeq2i |
⊢ ( ◡ 𝐹 “ ( 𝑆 ∩ ( V ∖ { 𝑍 } ) ) ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) |
21 |
18 20
|
eqtr3di |
⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ) |
22 |
21
|
adantl |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ) |
23 |
7 22
|
eqtrd |
⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ) |
24 |
23
|
ex |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ) ) |