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

Theorem pwssun 4944
 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 3748 . . . . . 6 (𝐵𝐴 ↔ (𝐴𝐵) = 𝐴)
2 pweq 4111 . . . . . . 7 ((𝐴𝐵) = 𝐴 → 𝒫 (𝐴𝐵) = 𝒫 𝐴)
3 eqimss 3620 . . . . . . 7 (𝒫 (𝐴𝐵) = 𝒫 𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
42, 3syl 17 . . . . . 6 ((𝐴𝐵) = 𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
51, 4sylbi 206 . . . . 5 (𝐵𝐴 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴)
6 ssequn1 3745 . . . . . 6 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
7 pweq 4111 . . . . . . 7 ((𝐴𝐵) = 𝐵 → 𝒫 (𝐴𝐵) = 𝒫 𝐵)
8 eqimss 3620 . . . . . . 7 (𝒫 (𝐴𝐵) = 𝒫 𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
97, 8syl 17 . . . . . 6 ((𝐴𝐵) = 𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
106, 9sylbi 206 . . . . 5 (𝐴𝐵 → 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵)
115, 10orim12i 537 . . . 4 ((𝐵𝐴𝐴𝐵) → (𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵))
1211orcoms 403 . . 3 ((𝐴𝐵𝐵𝐴) → (𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵))
13 ssun 3754 . . 3 ((𝒫 (𝐴𝐵) ⊆ 𝒫 𝐴 ∨ 𝒫 (𝐴𝐵) ⊆ 𝒫 𝐵) → 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
1412, 13syl 17 . 2 ((𝐴𝐵𝐵𝐴) → 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
15 vex 3176 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
1615snss 4259 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴 ↔ {𝑥} ⊆ 𝐴)
17 vex 3176 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
1817snss 4259 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐵 ↔ {𝑦} ⊆ 𝐵)
19 unss12 3747 . . . . . . . . . . . . . . . . . . 19 (({𝑥} ⊆ 𝐴 ∧ {𝑦} ⊆ 𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
2016, 18, 19syl2anb 495 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐴𝑦𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
21 zfpair2 4834 . . . . . . . . . . . . . . . . . . . 20 {𝑥, 𝑦} ∈ V
2221elpw 4114 . . . . . . . . . . . . . . . . . . 19 ({𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵) ↔ {𝑥, 𝑦} ⊆ (𝐴𝐵))
23 df-pr 4128 . . . . . . . . . . . . . . . . . . . 20 {𝑥, 𝑦} = ({𝑥} ∪ {𝑦})
2423sseq1i 3592 . . . . . . . . . . . . . . . . . . 19 ({𝑥, 𝑦} ⊆ (𝐴𝐵) ↔ ({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵))
2522, 24bitr2i 264 . . . . . . . . . . . . . . . . . 18 (({𝑥} ∪ {𝑦}) ⊆ (𝐴𝐵) ↔ {𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵))
2620, 25sylib 207 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑦𝐵) → {𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵))
27 ssel 3562 . . . . . . . . . . . . . . . . 17 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → ({𝑥, 𝑦} ∈ 𝒫 (𝐴𝐵) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵)))
2826, 27syl5 33 . . . . . . . . . . . . . . . 16 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → ((𝑥𝐴𝑦𝐵) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵)))
2928expcomd 453 . . . . . . . . . . . . . . 15 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (𝑥𝐴 → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵))))
3029imp31 447 . . . . . . . . . . . . . 14 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → {𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵))
31 elun 3715 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ (𝒫 𝐴 ∪ 𝒫 𝐵) ↔ ({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵))
3230, 31sylib 207 . . . . . . . . . . . . 13 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → ({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵))
3321elpw 4114 . . . . . . . . . . . . . . . 16 ({𝑥, 𝑦} ∈ 𝒫 𝐴 ↔ {𝑥, 𝑦} ⊆ 𝐴)
3415, 17prss 4291 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑦𝐴) ↔ {𝑥, 𝑦} ⊆ 𝐴)
3533, 34bitr4i 266 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} ∈ 𝒫 𝐴 ↔ (𝑥𝐴𝑦𝐴))
3635simprbi 479 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ 𝒫 𝐴𝑦𝐴)
3721elpw 4114 . . . . . . . . . . . . . . . 16 ({𝑥, 𝑦} ∈ 𝒫 𝐵 ↔ {𝑥, 𝑦} ⊆ 𝐵)
3815, 17prss 4291 . . . . . . . . . . . . . . . 16 ((𝑥𝐵𝑦𝐵) ↔ {𝑥, 𝑦} ⊆ 𝐵)
3937, 38bitr4i 266 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} ∈ 𝒫 𝐵 ↔ (𝑥𝐵𝑦𝐵))
4039simplbi 475 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} ∈ 𝒫 𝐵𝑥𝐵)
4136, 40orim12i 537 . . . . . . . . . . . . 13 (({𝑥, 𝑦} ∈ 𝒫 𝐴 ∨ {𝑥, 𝑦} ∈ 𝒫 𝐵) → (𝑦𝐴𝑥𝐵))
4232, 41syl 17 . . . . . . . . . . . 12 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → (𝑦𝐴𝑥𝐵))
4342ord 391 . . . . . . . . . . 11 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝐴) → (¬ 𝑦𝐴𝑥𝐵))
4443impancom 455 . . . . . . . . . 10 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ ¬ 𝑦𝐴) → (𝑥𝐴𝑥𝐵))
4544ssrdv 3574 . . . . . . . . 9 (((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ 𝑦𝐵) ∧ ¬ 𝑦𝐴) → 𝐴𝐵)
4645exp31 628 . . . . . . . 8 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (¬ 𝑦𝐴𝐴𝐵)))
47 con1b 347 . . . . . . . 8 ((¬ 𝑦𝐴𝐴𝐵) ↔ (¬ 𝐴𝐵𝑦𝐴))
4846, 47syl6ib 240 . . . . . . 7 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝑦𝐵 → (¬ 𝐴𝐵𝑦𝐴)))
4948com23 84 . . . . . 6 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (¬ 𝐴𝐵 → (𝑦𝐵𝑦𝐴)))
5049imp 444 . . . . 5 ((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ ¬ 𝐴𝐵) → (𝑦𝐵𝑦𝐴))
5150ssrdv 3574 . . . 4 ((𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ ¬ 𝐴𝐵) → 𝐵𝐴)
5251ex 449 . . 3 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (¬ 𝐴𝐵𝐵𝐴))
5352orrd 392 . 2 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) → (𝐴𝐵𝐵𝐴))
5414, 53impbii 198 1 ((𝐴𝐵𝐵𝐴) ↔ 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ∪ cun 3538   ⊆ wss 3540  𝒫 cpw 4108  {csn 4125  {cpr 4127 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-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-un 3545  df-in 3547  df-ss 3554  df-pw 4110  df-sn 4126  df-pr 4128 This theorem is referenced by:  pwun  4946
 Copyright terms: Public domain W3C validator