Description: The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of Kunen p. 31. (Contributed by Raph Levien, 4-Dec-2003) (Proof shortened by AV, 16-Jun-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | mapex | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : 𝐴 ⟶ 𝐵 ) } = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : 𝐴 ⟶ 𝐵 ) } | |
2 | 1 | fabexg | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : 𝐴 ⟶ 𝐵 ) } ∈ V ) |
3 | id | ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 ) | |
4 | 3 | ancli | ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : 𝐴 ⟶ 𝐵 ) ) |
5 | 4 | ss2abi | ⊢ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ⊆ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : 𝐴 ⟶ 𝐵 ) } |
6 | 5 | a1i | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ⊆ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : 𝐴 ⟶ 𝐵 ) } ) |
7 | 2 6 | ssexd | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V ) |