Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sspwb | Structured version Visualization version GIF version |
Description: Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
Ref | Expression |
---|---|
sspwb | ⊢ (𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr2 3575 | . . . . 5 ⊢ (𝑥 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝑥 ⊆ 𝐵)) | |
2 | 1 | com12 32 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵)) |
3 | vex 3176 | . . . . 5 ⊢ 𝑥 ∈ V | |
4 | 3 | elpw 4114 | . . . 4 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
5 | 3 | elpw 4114 | . . . 4 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵) |
6 | 2, 4, 5 | 3imtr4g 284 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)) |
7 | 6 | ssrdv 3574 | . 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
8 | ssel 3562 | . . . 4 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 → ({𝑥} ∈ 𝒫 𝐴 → {𝑥} ∈ 𝒫 𝐵)) | |
9 | snex 4835 | . . . . . 6 ⊢ {𝑥} ∈ V | |
10 | 9 | elpw 4114 | . . . . 5 ⊢ ({𝑥} ∈ 𝒫 𝐴 ↔ {𝑥} ⊆ 𝐴) |
11 | 3 | snss 4259 | . . . . 5 ⊢ (𝑥 ∈ 𝐴 ↔ {𝑥} ⊆ 𝐴) |
12 | 10, 11 | bitr4i 266 | . . . 4 ⊢ ({𝑥} ∈ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴) |
13 | 9 | elpw 4114 | . . . . 5 ⊢ ({𝑥} ∈ 𝒫 𝐵 ↔ {𝑥} ⊆ 𝐵) |
14 | 3 | snss 4259 | . . . . 5 ⊢ (𝑥 ∈ 𝐵 ↔ {𝑥} ⊆ 𝐵) |
15 | 13, 14 | bitr4i 266 | . . . 4 ⊢ ({𝑥} ∈ 𝒫 𝐵 ↔ 𝑥 ∈ 𝐵) |
16 | 8, 12, 15 | 3imtr3g 283 | . . 3 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
17 | 16 | ssrdv 3574 | . 2 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 → 𝐴 ⊆ 𝐵) |
18 | 7, 17 | impbii 198 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∈ wcel 1977 ⊆ wss 3540 𝒫 cpw 4108 {csn 4125 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-pw 4110 df-sn 4126 df-pr 4128 |
This theorem is referenced by: pwel 4847 ssextss 4849 pweqb 4852 pwdom 7997 marypha1lem 8222 wdompwdom 8366 r1pwss 8530 pwwf 8553 rankpwi 8569 rankxplim 8625 ackbij2lem1 8924 fictb 8950 ssfin2 9025 ssfin3ds 9035 ttukeylem2 9215 hashbclem 13093 wrdexg 13170 incexclem 14407 hashbcss 15546 isacs1i 16141 mreacs 16142 acsfn 16143 sscpwex 16298 wunfunc 16382 isacs3lem 16989 isacs5lem 16992 tgcmp 21014 imastopn 21333 fgabs 21493 fgtr 21504 trfg 21505 ssufl 21532 alexsubb 21660 tsmsres 21757 cfiluweak 21909 cfilresi 22901 cmetss 22921 minveclem4a 23009 minveclem4 23011 vitali 23188 sqff1o 24708 elsigagen2 29538 ldsysgenld 29550 ldgenpisyslem1 29553 measres 29612 imambfm 29651 ballotlem2 29877 neibastop1 31524 neibastop2lem 31525 neibastop2 31526 sstotbnd2 32743 isnacs3 36291 aomclem2 36643 dssmapnvod 37334 gneispace 37452 sge0less 39285 sge0iunmptlemre 39308 |
Copyright terms: Public domain | W3C validator |