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

Theorem pwssun 5049
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 3819 . . . . . 6 (𝐵𝐴 ↔ (𝐴𝐵) = 𝐴)
2 pweq 4194 . . . . . . 7 ((𝐴𝐵) = 𝐴 → 𝒫 (𝐴𝐵) = 𝒫 𝐴)
3 eqimss 3690 . . . . . . 7 (𝒫 (𝐴𝐵) = 𝒫 𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
42, 3syl 17 . . . . . 6 ((𝐴𝐵) = 𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
51, 4sylbi 207 . . . . 5 (𝐵𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
6 ssequn1 3816 . . . . . 6 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
7 pweq 4194 . . . . . . 7 ((𝐴𝐵) = 𝐵 → 𝒫 (𝐴𝐵) = 𝒫 𝐵)
8 eqimss 3690 . . . . . . 7 (𝒫 (𝐴𝐵) = 𝒫 𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
97, 8syl 17 . . . . . 6 ((𝐴𝐵) = 𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
106, 9sylbi 207 . . . . 5 (𝐴𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
115, 10orim12i 537 . . . 4 ((𝐵𝐴𝐴𝐵) → (𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵))
1211orcoms 403 . . 3 ((𝐴𝐵𝐵𝐴) → (𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵))
13 ssun 3825 . . 3 ((𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵) → 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
1412, 13syl 17 . 2 ((𝐴𝐵𝐵𝐴) → 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
15 vex 3234 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
1615snss 4348 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴 ↔ {𝑥} ⊆ 𝐴)
17 vex 3234 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
1817snss 4348 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐵 ↔ {𝑦} ⊆ 𝐵)
19 unss12 3818 . . . . . . . . . . . . . . . . . . 19 (({𝑥} ⊆ 𝐴 ∧ {𝑦} ⊆ 𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
2016, 18, 19syl2anb 495 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐴𝑦𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
21 zfpair2 4937 . . . . . . . . . . . . . . . . . . . 20 {𝑥, 𝑦} ∈ V
2221elpw 4197 . . . . . . . . . . . . . . . . . . 19 ({𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵) ↔ {𝑥, 𝑦} ⊆ (𝐴𝐵))
23 df-pr 4213 . . . . . . . . . . . . . . . . . . . 20 {𝑥, 𝑦} = ({𝑥} ∪ {𝑦})
2423sseq1i 3662 . . . . . . . . . . . . . . . . . . 19 ({𝑥, 𝑦} ⊆ (𝐴𝐵) ↔ ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
2522, 24bitr2i 265 . . . . . . . . . . . . . . . . . 18 (({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵) ↔ {𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵))
2620, 25sylib 208 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑦𝐵) → {𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵))
27 ssel 3630 . . . . . . . . . . . . . . . . 17 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → ({𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵)))
2826, 27syl5 34 . . . . . . . . . . . . . . . 16 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → ((𝑥𝐴𝑦𝐵) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵)))
2928expcomd 453 . . . . . . . . . . . . . . 15 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (𝑥𝐴 → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵))))
3029imp31 447 . . . . . . . . . . . . . 14 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵))
31 elun 3786 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵) ↔ ({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵))
3230, 31sylib 208 . . . . . . . . . . . . 13 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → ({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵))
3321elpw 4197 . . . . . . . . . . . . . . . 16 ({𝑥, 𝑦} ∈ 𝒫 𝐴 ↔ {𝑥, 𝑦} ⊆ 𝐴)
3415, 17prss 4383 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑦𝐴) ↔ {𝑥, 𝑦} ⊆ 𝐴)
3533, 34bitr4i 267 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} ∈ 𝒫 𝐴 ↔ (𝑥𝐴𝑦𝐴))
3635simprbi 479 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ 𝒫 𝐴𝑦𝐴)
3721elpw 4197 . . . . . . . . . . . . . . . 16 ({𝑥, 𝑦} ∈ 𝒫 𝐵 ↔ {𝑥, 𝑦} ⊆ 𝐵)
3815, 17prss 4383 . . . . . . . . . . . . . . . 16 ((𝑥𝐵𝑦𝐵) ↔ {𝑥, 𝑦} ⊆ 𝐵)
3937, 38bitr4i 267 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} ∈ 𝒫 𝐵 ↔ (𝑥𝐵𝑦𝐵))
4039simplbi 475 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ 𝒫 𝐵𝑥𝐵)
4136, 40orim12i 537 . . . . . . . . . . . . 13 (({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵) → (𝑦𝐴𝑥𝐵))
4232, 41syl 17 . . . . . . . . . . . 12 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → (𝑦𝐴𝑥𝐵))
4342ord 391 . . . . . . . . . . 11 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → (¬ 𝑦𝐴𝑥𝐵))
4443impancom 455 . . . . . . . . . 10 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ ¬ 𝑦𝐴) → (𝑥𝐴𝑥𝐵))
4544ssrdv 3642 . . . . . . . . 9 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ ¬ 𝑦𝐴) → 𝐴𝐵)
4645exp31 629 . . . . . . . 8 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (¬ 𝑦𝐴𝐴𝐵)))
47 con1b 347 . . . . . . . 8 ((¬ 𝑦𝐴𝐴𝐵) ↔ (¬ 𝐴𝐵𝑦𝐴))
4846, 47syl6ib 241 . . . . . . 7 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (¬ 𝐴𝐵𝑦𝐴)))
4948com23 86 . . . . . 6 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (¬ 𝐴𝐵 → (𝑦𝐵𝑦𝐴)))
5049imp 444 . . . . 5 ((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ ¬ 𝐴𝐵) → (𝑦𝐵𝑦𝐴))
5150ssrdv 3642 . . . 4 ((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ ¬ 𝐴𝐵) → 𝐵𝐴)
5251ex 449 . . 3 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (¬ 𝐴𝐵𝐵𝐴))
5352orrd 392 . 2 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝐴𝐵𝐵𝐴))
5414, 53impbii 199 1 ((𝐴𝐵𝐵𝐴) ↔ 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  cun 3605  wss 3607  𝒫 cpw 4191  {csn 4210  {cpr 4212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614  df-ss 3621  df-pw 4193  df-sn 4211  df-pr 4213
This theorem is referenced by:  pwun  5051
  Copyright terms: Public domain W3C validator