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

Theorem pwssun 5448
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 4156 . . . . . 6 (𝐵𝐴 ↔ (𝐴𝐵) = 𝐴)
2 pweq 4538 . . . . . . 7 ((𝐴𝐵) = 𝐴 → 𝒫 (𝐴𝐵) = 𝒫 𝐴)
3 eqimss 4020 . . . . . . 7 (𝒫 (𝐴𝐵) = 𝒫 𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
42, 3syl 17 . . . . . 6 ((𝐴𝐵) = 𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
51, 4sylbi 218 . . . . 5 (𝐵𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
6 ssequn1 4153 . . . . . 6 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
7 pweq 4538 . . . . . . 7 ((𝐴𝐵) = 𝐵 → 𝒫 (𝐴𝐵) = 𝒫 𝐵)
8 eqimss 4020 . . . . . . 7 (𝒫 (𝐴𝐵) = 𝒫 𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
97, 8syl 17 . . . . . 6 ((𝐴𝐵) = 𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
106, 9sylbi 218 . . . . 5 (𝐴𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
115, 10orim12i 902 . . . 4 ((𝐵𝐴𝐴𝐵) → (𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵))
1211orcoms 868 . . 3 ((𝐴𝐵𝐵𝐴) → (𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵))
13 ssun 4162 . . 3 ((𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵) → 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
1412, 13syl 17 . 2 ((𝐴𝐵𝐵𝐴) → 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
15 vex 3495 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
1615snss 4710 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴 ↔ {𝑥} ⊆ 𝐴)
17 vex 3495 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
1817snss 4710 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐵 ↔ {𝑦} ⊆ 𝐵)
19 unss12 4155 . . . . . . . . . . . . . . . . . . 19 (({𝑥} ⊆ 𝐴 ∧ {𝑦} ⊆ 𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
2016, 18, 19syl2anb 597 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐴𝑦𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
21 zfpair2 5321 . . . . . . . . . . . . . . . . . . . 20 {𝑥, 𝑦} ∈ V
2221elpw 4542 . . . . . . . . . . . . . . . . . . 19 ({𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵) ↔ {𝑥, 𝑦} ⊆ (𝐴𝐵))
23 df-pr 4560 . . . . . . . . . . . . . . . . . . . 20 {𝑥, 𝑦} = ({𝑥} ∪ {𝑦})
2423sseq1i 3992 . . . . . . . . . . . . . . . . . . 19 ({𝑥, 𝑦} ⊆ (𝐴𝐵) ↔ ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
2522, 24bitr2i 277 . . . . . . . . . . . . . . . . . 18 (({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵) ↔ {𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵))
2620, 25sylib 219 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑦𝐵) → {𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵))
27 ssel 3958 . . . . . . . . . . . . . . . . 17 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → ({𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵)))
2826, 27syl5 34 . . . . . . . . . . . . . . . 16 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → ((𝑥𝐴𝑦𝐵) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵)))
2928expcomd 417 . . . . . . . . . . . . . . 15 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (𝑥𝐴 → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵))))
3029imp31 418 . . . . . . . . . . . . . 14 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵))
31 elun 4122 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵) ↔ ({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵))
3230, 31sylib 219 . . . . . . . . . . . . 13 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → ({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵))
3321elpw 4542 . . . . . . . . . . . . . . . 16 ({𝑥, 𝑦} ∈ 𝒫 𝐴 ↔ {𝑥, 𝑦} ⊆ 𝐴)
3415, 17prss 4745 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑦𝐴) ↔ {𝑥, 𝑦} ⊆ 𝐴)
3533, 34bitr4i 279 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} ∈ 𝒫 𝐴 ↔ (𝑥𝐴𝑦𝐴))
3635simprbi 497 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ 𝒫 𝐴𝑦𝐴)
3721elpw 4542 . . . . . . . . . . . . . . . 16 ({𝑥, 𝑦} ∈ 𝒫 𝐵 ↔ {𝑥, 𝑦} ⊆ 𝐵)
3815, 17prss 4745 . . . . . . . . . . . . . . . 16 ((𝑥𝐵𝑦𝐵) ↔ {𝑥, 𝑦} ⊆ 𝐵)
3937, 38bitr4i 279 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} ∈ 𝒫 𝐵 ↔ (𝑥𝐵𝑦𝐵))
4039simplbi 498 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ 𝒫 𝐵𝑥𝐵)
4136, 40orim12i 902 . . . . . . . . . . . . 13 (({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵) → (𝑦𝐴𝑥𝐵))
4232, 41syl 17 . . . . . . . . . . . 12 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → (𝑦𝐴𝑥𝐵))
4342ord 858 . . . . . . . . . . 11 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → (¬ 𝑦𝐴𝑥𝐵))
4443impancom 452 . . . . . . . . . 10 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ ¬ 𝑦𝐴) → (𝑥𝐴𝑥𝐵))
4544ssrdv 3970 . . . . . . . . 9 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ ¬ 𝑦𝐴) → 𝐴𝐵)
4645exp31 420 . . . . . . . 8 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (¬ 𝑦𝐴𝐴𝐵)))
47 con1b 360 . . . . . . . 8 ((¬ 𝑦𝐴𝐴𝐵) ↔ (¬ 𝐴𝐵𝑦𝐴))
4846, 47syl6ib 252 . . . . . . 7 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (¬ 𝐴𝐵𝑦𝐴)))
4948com23 86 . . . . . 6 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (¬ 𝐴𝐵 → (𝑦𝐵𝑦𝐴)))
5049imp 407 . . . . 5 ((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ ¬ 𝐴𝐵) → (𝑦𝐵𝑦𝐴))
5150ssrdv 3970 . . . 4 ((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ ¬ 𝐴𝐵) → 𝐵𝐴)
5251ex 413 . . 3 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (¬ 𝐴𝐵𝐵𝐴))
5352orrd 857 . 2 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝐴𝐵𝐵𝐴))
5414, 53impbii 210 1 ((𝐴𝐵𝐵𝐴) ↔ 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wcel 2105  cun 3931  wss 3933  𝒫 cpw 4535  {csn 4557  {cpr 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-in 3940  df-ss 3949  df-pw 4537  df-sn 4558  df-pr 4560
This theorem is referenced by:  pwun  5451
  Copyright terms: Public domain W3C validator