Description: Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mnutrcld.1 | ⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) } | |
mnutrcld.2 | ⊢ ( 𝜑 → 𝑈 ∈ 𝑀 ) | ||
mnutrcld.3 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) | ||
mnutrcld.4 | ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 ) | ||
Assertion | mnutrcld | ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mnutrcld.1 | ⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) } | |
2 | mnutrcld.2 | ⊢ ( 𝜑 → 𝑈 ∈ 𝑀 ) | |
3 | mnutrcld.3 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) | |
4 | mnutrcld.4 | ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 ) | |
5 | 1 2 3 | mnuunid | ⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝑈 ) |
6 | elssuni | ⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝐴 ) | |
7 | 4 6 | syl | ⊢ ( 𝜑 → 𝐵 ⊆ ∪ 𝐴 ) |
8 | 1 2 5 7 | mnussd | ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 ) |