Step |
Hyp |
Ref |
Expression |
1 |
|
ndfatafv2 |
⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 ) |
2 |
|
pwuninel |
⊢ ¬ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹 |
3 |
|
df-nel |
⊢ ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ↔ ¬ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ) |
4 |
|
eleq1 |
⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ↔ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹 ) ) |
5 |
4
|
notbid |
⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 → ( ¬ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ↔ ¬ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹 ) ) |
6 |
3 5
|
syl5bb |
⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ↔ ¬ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹 ) ) |
7 |
2 6
|
mpbiri |
⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) |
8 |
1 7
|
syl |
⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) |