Description: Function value when F is (locally) not a function. Theorem 6.12(2) of TakeutiZaring p. 27, analogous to tz6.12-2 . (Contributed by AV, 5-Sep-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | tz6.12-2-afv2 | ⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfdfat2 | ⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) ) | |
2 | 1 | simprbi | ⊢ ( 𝐹 defAt 𝐴 → ∃! 𝑥 𝐴 𝐹 𝑥 ) |
3 | ndfatafv2nrn | ⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) | |
4 | 2 3 | nsyl5 | ⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) |