Step |
Hyp |
Ref |
Expression |
1 |
|
suppssrg.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
2 |
|
suppssrg.n |
⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 ) |
3 |
|
suppssrg.a |
⊢ ( 𝜑 → 𝐹 ∈ 𝑉 ) |
4 |
|
suppssrg.z |
⊢ ( 𝜑 → 𝑍 ∈ 𝑈 ) |
5 |
|
eldif |
⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝑊 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊 ) ) |
6 |
1
|
ffnd |
⊢ ( 𝜑 → 𝐹 Fn 𝐴 ) |
7 |
|
elsuppfng |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑈 ) → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) ) |
8 |
6 3 4 7
|
syl3anc |
⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) ) |
9 |
2
|
sseld |
⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) → 𝑋 ∈ 𝑊 ) ) |
10 |
8 9
|
sylbird |
⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) → 𝑋 ∈ 𝑊 ) ) |
11 |
10
|
expdimp |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 → 𝑋 ∈ 𝑊 ) ) |
12 |
11
|
necon1bd |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ¬ 𝑋 ∈ 𝑊 → ( 𝐹 ‘ 𝑋 ) = 𝑍 ) ) |
13 |
12
|
impr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑍 ) |
14 |
5 13
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑍 ) |