Description: A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | wun0.1 | ⊢ ( 𝜑 → 𝑈 ∈ WUni ) | |
wunop.2 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) | ||
wunop.3 | ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 ) | ||
Assertion | wunpm | ⊢ ( 𝜑 → ( 𝐴 ↑pm 𝐵 ) ∈ 𝑈 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wun0.1 | ⊢ ( 𝜑 → 𝑈 ∈ WUni ) | |
2 | wunop.2 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) | |
3 | wunop.3 | ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 ) | |
4 | 1 3 2 | wunxp | ⊢ ( 𝜑 → ( 𝐵 × 𝐴 ) ∈ 𝑈 ) |
5 | 1 4 | wunpw | ⊢ ( 𝜑 → 𝒫 ( 𝐵 × 𝐴 ) ∈ 𝑈 ) |
6 | pmsspw | ⊢ ( 𝐴 ↑pm 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 ) | |
7 | 6 | a1i | ⊢ ( 𝜑 → ( 𝐴 ↑pm 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 ) ) |
8 | 1 5 7 | wunss | ⊢ ( 𝜑 → ( 𝐴 ↑pm 𝐵 ) ∈ 𝑈 ) |