Description: The set of functions with a proper class as domain is empty. (Contributed by AV, 22-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | fsetdmprc0 | ⊢ ( 𝐴 ∉ V → { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nel | ⊢ ( 𝐴 ∉ V ↔ ¬ 𝐴 ∈ V ) | |
2 | vex | ⊢ 𝑓 ∈ V | |
3 | 2 | a1i | ⊢ ( 𝑓 Fn 𝐴 → 𝑓 ∈ V ) |
4 | id | ⊢ ( 𝑓 Fn 𝐴 → 𝑓 Fn 𝐴 ) | |
5 | 3 4 | fndmexd | ⊢ ( 𝑓 Fn 𝐴 → 𝐴 ∈ V ) |
6 | 5 | con3i | ⊢ ( ¬ 𝐴 ∈ V → ¬ 𝑓 Fn 𝐴 ) |
7 | 1 6 | sylbi | ⊢ ( 𝐴 ∉ V → ¬ 𝑓 Fn 𝐴 ) |
8 | 7 | alrimiv | ⊢ ( 𝐴 ∉ V → ∀ 𝑓 ¬ 𝑓 Fn 𝐴 ) |
9 | ab0 | ⊢ ( { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ ↔ ∀ 𝑓 ¬ 𝑓 Fn 𝐴 ) | |
10 | 8 9 | sylibr | ⊢ ( 𝐴 ∉ V → { 𝑓 ∣ 𝑓 Fn 𝐴 } = ∅ ) |