MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sspwb Structured version   Visualization version   GIF version

Theorem sspwb 5338
Description: The powerclass construction preserves and reflects inclusion. Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
Assertion
Ref Expression
sspwb (𝐴𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵)

Proof of Theorem sspwb
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 sstr2 3978 . . . . 5 (𝑥𝐴 → (𝐴𝐵𝑥𝐵))
21com12 32 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
3 vex 3503 . . . . 5 𝑥 ∈ V
43elpw 4549 . . . 4 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
53elpw 4549 . . . 4 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
62, 4, 53imtr4g 297 . . 3 (𝐴𝐵 → (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵))
76ssrdv 3977 . 2 (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
8 ssel 3965 . . . 4 (𝒫 𝐴 ⊆ 𝒫 𝐵 → ({𝑥} ∈ 𝒫 𝐴 → {𝑥} ∈ 𝒫 𝐵))
9 snex 5328 . . . . . 6 {𝑥} ∈ V
109elpw 4549 . . . . 5 ({𝑥} ∈ 𝒫 𝐴 ↔ {𝑥} ⊆ 𝐴)
113snss 4717 . . . . 5 (𝑥𝐴 ↔ {𝑥} ⊆ 𝐴)
1210, 11bitr4i 279 . . . 4 ({𝑥} ∈ 𝒫 𝐴𝑥𝐴)
139elpw 4549 . . . . 5 ({𝑥} ∈ 𝒫 𝐵 ↔ {𝑥} ⊆ 𝐵)
143snss 4717 . . . . 5 (𝑥𝐵 ↔ {𝑥} ⊆ 𝐵)
1513, 14bitr4i 279 . . . 4 ({𝑥} ∈ 𝒫 𝐵𝑥𝐵)
168, 12, 153imtr3g 296 . . 3 (𝒫 𝐴 ⊆ 𝒫 𝐵 → (𝑥𝐴𝑥𝐵))
1716ssrdv 3977 . 2 (𝒫 𝐴 ⊆ 𝒫 𝐵𝐴𝐵)
187, 17impbii 210 1 (𝐴𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wcel 2107  wss 3940  𝒫 cpw 4542  {csn 4564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-pw 4544  df-sn 4565  df-pr 4567
This theorem is referenced by:  pwel  5341  ssextss  5343  pweqb  5346  pwunss  5452  pwundif  5455  pwdom  8663  marypha1lem  8891  wdompwdom  9036  r1pwss  9207  pwwf  9230  rankpwi  9246  rankxplim  9302  ackbij2lem1  9635  fictb  9661  ssfin2  9736  ssfin3ds  9746  ttukeylem2  9926  hashbclem  13805  wrdexgOLD  13867  incexclem  15186  hashbcss  16335  isacs1i  16923  mreacs  16924  acsfn  16925  sscpwex  17080  wunfunc  17164  isacs3lem  17771  isacs5lem  17774  tgcmp  21944  imastopn  22263  fgabs  22422  fgtr  22433  trfg  22434  ssufl  22461  alexsubb  22589  tsmsres  22686  cfiluweak  22838  cfilresi  23832  cmetss  23853  minveclem4a  23967  minveclem4  23969  vitali  24148  sqff1o  25692  elsigagen2  31312  ldsysgenld  31324  ldgenpisyslem1  31327  measres  31386  imambfm  31425  ballotlem2  31651  neibastop1  33610  neibastop2lem  33611  neibastop2  33612  sstotbnd2  34939  psspwb  38998  isnacs3  39191  aomclem2  39539  dssmapnvod  40250  gneispace  40368  sge0less  42559  sge0iunmptlemre  42582
  Copyright terms: Public domain W3C validator