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 ) |