Description: Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mnussd.1 | ⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) } | |
mnussd.2 | ⊢ ( 𝜑 → 𝑈 ∈ 𝑀 ) | ||
mnussd.3 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) | ||
mnussd.4 | ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 ) | ||
Assertion | mnussd | ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mnussd.1 | ⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) } | |
2 | mnussd.2 | ⊢ ( 𝜑 → 𝑈 ∈ 𝑀 ) | |
3 | mnussd.3 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) | |
4 | mnussd.4 | ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 ) | |
5 | 1 2 3 | mnuop123d | ⊢ ( 𝜑 → ( 𝒫 𝐴 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) |
6 | 5 | simpld | ⊢ ( 𝜑 → 𝒫 𝐴 ⊆ 𝑈 ) |
7 | 3 4 | sselpwd | ⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝐴 ) |
8 | 6 7 | sseldd | ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 ) |