Step |
Hyp |
Ref |
Expression |
1 |
|
ffn |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 ) |
2 |
|
fnafv2elrn |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) |
3 |
1 2
|
sylan |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) |
4 |
3
|
ex |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐶 ∈ 𝐴 → ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) ) |
5 |
|
fdm |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 ) |
6 |
|
ndmafv2nrn |
⊢ ( ¬ 𝐶 ∈ dom 𝐹 → ( 𝐹 '''' 𝐶 ) ∉ ran 𝐹 ) |
7 |
|
df-nel |
⊢ ( ( 𝐹 '''' 𝐶 ) ∉ ran 𝐹 ↔ ¬ ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) |
8 |
6 7
|
sylib |
⊢ ( ¬ 𝐶 ∈ dom 𝐹 → ¬ ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) |
9 |
8
|
con4i |
⊢ ( ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 → 𝐶 ∈ dom 𝐹 ) |
10 |
|
eleq2 |
⊢ ( dom 𝐹 = 𝐴 → ( 𝐶 ∈ dom 𝐹 ↔ 𝐶 ∈ 𝐴 ) ) |
11 |
9 10
|
syl5ib |
⊢ ( dom 𝐹 = 𝐴 → ( ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 → 𝐶 ∈ 𝐴 ) ) |
12 |
5 11
|
syl |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 → 𝐶 ∈ 𝐴 ) ) |
13 |
4 12
|
impbid |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐶 ∈ 𝐴 ↔ ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) ) |