Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > wunss | Structured version Visualization version GIF version |
Description: A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Ref | Expression |
---|---|
wununi.1 | ⊢ (𝜑 → 𝑈 ∈ WUni) |
wununi.2 | ⊢ (𝜑 → 𝐴 ∈ 𝑈) |
wunss.3 | ⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
Ref | Expression |
---|---|
wunss | ⊢ (𝜑 → 𝐵 ∈ 𝑈) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wununi.1 | . . 3 ⊢ (𝜑 → 𝑈 ∈ WUni) | |
2 | wununi.2 | . . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑈) | |
3 | 1, 2 | wunpw 10345 | . . 3 ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈) |
4 | 1, 3 | wunelss 10346 | . 2 ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝑈) |
5 | wunss.3 | . . 3 ⊢ (𝜑 → 𝐵 ⊆ 𝐴) | |
6 | 2, 5 | sselpwd 5233 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐴) |
7 | 4, 6 | sseldd 3916 | 1 ⊢ (𝜑 → 𝐵 ∈ 𝑈) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2111 ⊆ wss 3880 𝒫 cpw 4527 WUnicwun 10338 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-11 2159 ax-ext 2709 ax-sep 5206 |
This theorem depends on definitions: df-bi 210 df-an 400 df-3an 1091 df-tru 1546 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-ne 2942 df-ral 3067 df-rab 3071 df-v 3422 df-in 3887 df-ss 3897 df-pw 4529 df-uni 4834 df-tr 5176 df-wun 10340 |
This theorem is referenced by: wunin 10351 wundif 10352 wunint 10353 wun0 10356 wunom 10358 wunxp 10362 wunpm 10363 wunmap 10364 wundm 10366 wunrn 10367 wuncnv 10368 wunres 10369 wunfv 10370 wunco 10371 wuntpos 10372 wuncn 10808 wunstr 16765 wunndx 16770 wunfunc 17429 wunfuncOLD 17430 |
Copyright terms: Public domain | W3C validator |