Metamath Proof Explorer

Theorem pwssun

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)

Ref Expression
Assertion pwssun ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ssequn2 ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐴 )
2 pweq ⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐴 → 𝒫 ( 𝐴 ∪ 𝐵 ) = 𝒫 𝐴 )
3 eqimss ⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) = 𝒫 𝐴 → 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐴 )
4 2 3 syl ⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐴 → 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐴 )
5 1 4 sylbi ⊢ ( 𝐵 ⊆ 𝐴 → 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐴 )
6 ssequn1 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐵 )
7 pweq ⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐵 → 𝒫 ( 𝐴 ∪ 𝐵 ) = 𝒫 𝐵 )
8 eqimss ⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) = 𝒫 𝐵 → 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐵 )
9 7 8 syl ⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐵 → 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐵 )
10 6 9 sylbi ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐵 )
11 5 10 orim12i ⊢ ( ( 𝐵 ⊆ 𝐴 ∨ 𝐴 ⊆ 𝐵 ) → ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐴 ∨ 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐵 ) )
12 11 orcoms ⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) → ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐴 ∨ 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐵 ) )
13 ssun ⊢ ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐴 ∨ 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝐵 ) → 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) )
14 12 13 syl ⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) → 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) )
15 vex ⊢ 𝑥 ∈ V
16 15 snss ⊢ ( 𝑥 ∈ 𝐴 ↔ { 𝑥 } ⊆ 𝐴 )
17 vex ⊢ 𝑦 ∈ V
18 17 snss ⊢ ( 𝑦 ∈ 𝐵 ↔ { 𝑦 } ⊆ 𝐵 )
19 unss12 ⊢ ( ( { 𝑥 } ⊆ 𝐴 ∧ { 𝑦 } ⊆ 𝐵 ) → ( { 𝑥 } ∪ { 𝑦 } ) ⊆ ( 𝐴 ∪ 𝐵 ) )
20 16 18 19 syl2anb ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( { 𝑥 } ∪ { 𝑦 } ) ⊆ ( 𝐴 ∪ 𝐵 ) )
21 zfpair2 ⊢ { 𝑥 , 𝑦 } ∈ V
22 21 elpw ⊢ ( { 𝑥 , 𝑦 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ ( 𝐴 ∪ 𝐵 ) )
23 df-pr ⊢ { 𝑥 , 𝑦 } = ( { 𝑥 } ∪ { 𝑦 } )
24 23 sseq1i ⊢ ( { 𝑥 , 𝑦 } ⊆ ( 𝐴 ∪ 𝐵 ) ↔ ( { 𝑥 } ∪ { 𝑦 } ) ⊆ ( 𝐴 ∪ 𝐵 ) )
25 22 24 bitr2i ⊢ ( ( { 𝑥 } ∪ { 𝑦 } ) ⊆ ( 𝐴 ∪ 𝐵 ) ↔ { 𝑥 , 𝑦 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) )
26 20 25 sylib ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 , 𝑦 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) )
27 ssel ⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) → ( { 𝑥 , 𝑦 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) → { 𝑥 , 𝑦 } ∈ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ) )
28 26 27 syl5 ⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 , 𝑦 } ∈ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ) )
29 28 expcomd ⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) → ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → { 𝑥 , 𝑦 } ∈ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ) ) )
30 29 imp31 ⊢ ( ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 , 𝑦 } ∈ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) )
31 elun ⊢ ( { 𝑥 , 𝑦 } ∈ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝒫 𝐴 ∨ { 𝑥 , 𝑦 } ∈ 𝒫 𝐵 ) )
32 30 31 sylib ⊢ ( ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( { 𝑥 , 𝑦 } ∈ 𝒫 𝐴 ∨ { 𝑥 , 𝑦 } ∈ 𝒫 𝐵 ) )
33 21 elpw ⊢ ( { 𝑥 , 𝑦 } ∈ 𝒫 𝐴 ↔ { 𝑥 , 𝑦 } ⊆ 𝐴 )
34 15 17 prss ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐴 )
35 33 34 bitr4i ⊢ ( { 𝑥 , 𝑦 } ∈ 𝒫 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
36 35 simprbi ⊢ ( { 𝑥 , 𝑦 } ∈ 𝒫 𝐴 → 𝑦 ∈ 𝐴 )
37 21 elpw ⊢ ( { 𝑥 , 𝑦 } ∈ 𝒫 𝐵 ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 )
38 15 17 prss ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 )
39 37 38 bitr4i ⊢ ( { 𝑥 , 𝑦 } ∈ 𝒫 𝐵 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
40 39 simplbi ⊢ ( { 𝑥 , 𝑦 } ∈ 𝒫 𝐵 → 𝑥 ∈ 𝐵 )
41 36 40 orim12i ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝒫 𝐴 ∨ { 𝑥 , 𝑦 } ∈ 𝒫 𝐵 ) → ( 𝑦 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
42 32 41 syl ⊢ ( ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
43 42 ord ⊢ ( ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
44 43 impancom ⊢ ( ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ¬ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
45 44 ssrdv ⊢ ( ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ¬ 𝑦 ∈ 𝐴 ) → 𝐴 ⊆ 𝐵 )
46 45 exp31 ⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) → ( 𝑦 ∈ 𝐵 → ( ¬ 𝑦 ∈ 𝐴 → 𝐴 ⊆ 𝐵 ) ) )
47 con1b ⊢ ( ( ¬ 𝑦 ∈ 𝐴 → 𝐴 ⊆ 𝐵 ) ↔ ( ¬ 𝐴 ⊆ 𝐵 → 𝑦 ∈ 𝐴 ) )
48 46 47 syl6ib ⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) → ( 𝑦 ∈ 𝐵 → ( ¬ 𝐴 ⊆ 𝐵 → 𝑦 ∈ 𝐴 ) ) )
49 48 com23 ⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) → ( ¬ 𝐴 ⊆ 𝐵 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐴 ) ) )
50 49 imp ⊢ ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ∧ ¬ 𝐴 ⊆ 𝐵 ) → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐴 ) )
51 50 ssrdv ⊢ ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ∧ ¬ 𝐴 ⊆ 𝐵 ) → 𝐵 ⊆ 𝐴 )
52 51 ex ⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) → ( ¬ 𝐴 ⊆ 𝐵 → 𝐵 ⊆ 𝐴 ) )
53 52 orrd ⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
54 14 53 impbii ⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) )