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

Theorem pwssun 4930
Description: The power class of the union of two classes is a subset of the union of their power classes, iff one class is a subclass of the other. Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
Assertion
Ref Expression
pwssun ((𝐴𝐵𝐵𝐴) ↔ 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))

Proof of Theorem pwssun
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssequn2 3743 . . . . . 6 (𝐵𝐴 ↔ (𝐴𝐵) = 𝐴)
2 pweq 4106 . . . . . . 7 ((𝐴𝐵) = 𝐴 → 𝒫 (𝐴𝐵) = 𝒫 𝐴)
3 eqimss 3615 . . . . . . 7 (𝒫 (𝐴𝐵) = 𝒫 𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
42, 3syl 17 . . . . . 6 ((𝐴𝐵) = 𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
51, 4sylbi 205 . . . . 5 (𝐵𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
6 ssequn1 3740 . . . . . 6 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
7 pweq 4106 . . . . . . 7 ((𝐴𝐵) = 𝐵 → 𝒫 (𝐴𝐵) = 𝒫 𝐵)
8 eqimss 3615 . . . . . . 7 (𝒫 (𝐴𝐵) = 𝒫 𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
97, 8syl 17 . . . . . 6 ((𝐴𝐵) = 𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
106, 9sylbi 205 . . . . 5 (𝐴𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
115, 10orim12i 536 . . . 4 ((𝐵𝐴𝐴𝐵) → (𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵))
1211orcoms 402 . . 3 ((𝐴𝐵𝐵𝐴) → (𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵))
13 ssun 3749 . . 3 ((𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵) → 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
1412, 13syl 17 . 2 ((𝐴𝐵𝐵𝐴) → 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
15 vex 3171 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
1615snss 4254 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴 ↔ {𝑥} ⊆ 𝐴)
17 vex 3171 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
1817snss 4254 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐵 ↔ {𝑦} ⊆ 𝐵)
19 unss12 3742 . . . . . . . . . . . . . . . . . . 19 (({𝑥} ⊆ 𝐴 ∧ {𝑦} ⊆ 𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
2016, 18, 19syl2anb 494 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐴𝑦𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
21 zfpair2 4825 . . . . . . . . . . . . . . . . . . . 20 {𝑥, 𝑦} ∈ V
2221elpw 4109 . . . . . . . . . . . . . . . . . . 19 ({𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵) ↔ {𝑥, 𝑦} ⊆ (𝐴𝐵))
23 df-pr 4123 . . . . . . . . . . . . . . . . . . . 20 {𝑥, 𝑦} = ({𝑥} ∪ {𝑦})
2423sseq1i 3587 . . . . . . . . . . . . . . . . . . 19 ({𝑥, 𝑦} ⊆ (𝐴𝐵) ↔ ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
2522, 24bitr2i 263 . . . . . . . . . . . . . . . . . 18 (({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵) ↔ {𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵))
2620, 25sylib 206 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑦𝐵) → {𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵))
27 ssel 3557 . . . . . . . . . . . . . . . . 17 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → ({𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵)))
2826, 27syl5 33 . . . . . . . . . . . . . . . 16 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → ((𝑥𝐴𝑦𝐵) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵)))
2928expcomd 452 . . . . . . . . . . . . . . 15 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (𝑥𝐴 → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵))))
3029imp31 446 . . . . . . . . . . . . . 14 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵))
31 elun 3710 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵) ↔ ({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵))
3230, 31sylib 206 . . . . . . . . . . . . 13 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → ({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵))
3321elpw 4109 . . . . . . . . . . . . . . . 16 ({𝑥, 𝑦} ∈ 𝒫 𝐴 ↔ {𝑥, 𝑦} ⊆ 𝐴)
3415, 17prss 4286 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑦𝐴) ↔ {𝑥, 𝑦} ⊆ 𝐴)
3533, 34bitr4i 265 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} ∈ 𝒫 𝐴 ↔ (𝑥𝐴𝑦𝐴))
3635simprbi 478 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ 𝒫 𝐴𝑦𝐴)
3721elpw 4109 . . . . . . . . . . . . . . . 16 ({𝑥, 𝑦} ∈ 𝒫 𝐵 ↔ {𝑥, 𝑦} ⊆ 𝐵)
3815, 17prss 4286 . . . . . . . . . . . . . . . 16 ((𝑥𝐵𝑦𝐵) ↔ {𝑥, 𝑦} ⊆ 𝐵)
3937, 38bitr4i 265 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} ∈ 𝒫 𝐵 ↔ (𝑥𝐵𝑦𝐵))
4039simplbi 474 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ 𝒫 𝐵𝑥𝐵)
4136, 40orim12i 536 . . . . . . . . . . . . 13 (({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵) → (𝑦𝐴𝑥𝐵))
4232, 41syl 17 . . . . . . . . . . . 12 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → (𝑦𝐴𝑥𝐵))
4342ord 390 . . . . . . . . . . 11 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → (¬ 𝑦𝐴𝑥𝐵))
4443impancom 454 . . . . . . . . . 10 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ ¬ 𝑦𝐴) → (𝑥𝐴𝑥𝐵))
4544ssrdv 3569 . . . . . . . . 9 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ ¬ 𝑦𝐴) → 𝐴𝐵)
4645exp31 627 . . . . . . . 8 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (¬ 𝑦𝐴𝐴𝐵)))
47 con1b 346 . . . . . . . 8 ((¬ 𝑦𝐴𝐴𝐵) ↔ (¬ 𝐴𝐵𝑦𝐴))
4846, 47syl6ib 239 . . . . . . 7 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (¬ 𝐴𝐵𝑦𝐴)))
4948com23 83 . . . . . 6 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (¬ 𝐴𝐵 → (𝑦𝐵𝑦𝐴)))
5049imp 443 . . . . 5 ((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ ¬ 𝐴𝐵) → (𝑦𝐵𝑦𝐴))
5150ssrdv 3569 . . . 4 ((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ ¬ 𝐴𝐵) → 𝐵𝐴)
5251ex 448 . . 3 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (¬ 𝐴𝐵𝐵𝐴))
5352orrd 391 . 2 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝐴𝐵𝐵𝐴))
5414, 53impbii 197 1 ((𝐴𝐵𝐵𝐴) ↔ 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382   = wceq 1474  wcel 1975  cun 3533  wss 3535  𝒫 cpw 4103  {csn 4120  {cpr 4122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-un 3540  df-in 3542  df-ss 3549  df-pw 4105  df-sn 4121  df-pr 4123
This theorem is referenced by:  pwun  4932
  Copyright terms: Public domain W3C validator