This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpsspw

Description: A Cartesian product is included in the power of the power of the union of its arguments. (Contributed by NM, 13-Sep-2006)

Ref Expression
Assertion xpsspw ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 )

Proof

Step Hyp Ref Expression
1 relxp ⊢ Rel ( 𝐴 × 𝐵 )
2 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
3 snssi ⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ⊆ 𝐴 )
4 ssun3 ⊢ ( { 𝑥 } ⊆ 𝐴 → { 𝑥 } ⊆ ( 𝐴 ∪ 𝐵 ) )
5 3 4 syl ⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ⊆ ( 𝐴 ∪ 𝐵 ) )
6 vsnex ⊢ { 𝑥 } ∈ V
7 6 elpw ⊢ ( { 𝑥 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) ↔ { 𝑥 } ⊆ ( 𝐴 ∪ 𝐵 ) )
8 5 7 sylibr ⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) )
9 8 adantr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) )
10 df-pr ⊢ { 𝑥 , 𝑦 } = ( { 𝑥 } ∪ { 𝑦 } )
11 snssi ⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ⊆ 𝐵 )
12 ssun4 ⊢ ( { 𝑦 } ⊆ 𝐵 → { 𝑦 } ⊆ ( 𝐴 ∪ 𝐵 ) )
13 11 12 syl ⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ⊆ ( 𝐴 ∪ 𝐵 ) )
14 5 13 anim12i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( { 𝑥 } ⊆ ( 𝐴 ∪ 𝐵 ) ∧ { 𝑦 } ⊆ ( 𝐴 ∪ 𝐵 ) ) )
15 unss ⊢ ( ( { 𝑥 } ⊆ ( 𝐴 ∪ 𝐵 ) ∧ { 𝑦 } ⊆ ( 𝐴 ∪ 𝐵 ) ) ↔ ( { 𝑥 } ∪ { 𝑦 } ) ⊆ ( 𝐴 ∪ 𝐵 ) )
16 14 15 sylib ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( { 𝑥 } ∪ { 𝑦 } ) ⊆ ( 𝐴 ∪ 𝐵 ) )
17 10 16 eqsstrid ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 , 𝑦 } ⊆ ( 𝐴 ∪ 𝐵 ) )
18 zfpair2 ⊢ { 𝑥 , 𝑦 } ∈ V
19 18 elpw ⊢ ( { 𝑥 , 𝑦 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ ( 𝐴 ∪ 𝐵 ) )
20 17 19 sylibr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 , 𝑦 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) )
21 9 20 jca ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( { 𝑥 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) ∧ { 𝑥 , 𝑦 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) ) )
22 prex ⊢ { { 𝑥 } , { 𝑥 , 𝑦 } } ∈ V
23 22 elpw ⊢ ( { { 𝑥 } , { 𝑥 , 𝑦 } } ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ↔ { { 𝑥 } , { 𝑥 , 𝑦 } } ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) )
24 vex ⊢ 𝑥 ∈ V
25 vex ⊢ 𝑦 ∈ V
26 24 25 dfop ⊢ ⟨ 𝑥 , 𝑦 ⟩ = { { 𝑥 } , { 𝑥 , 𝑦 } }
27 26 eleq1i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ↔ { { 𝑥 } , { 𝑥 , 𝑦 } } ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) )
28 6 18 prss ⊢ ( ( { 𝑥 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) ∧ { 𝑥 , 𝑦 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) ) ↔ { { 𝑥 } , { 𝑥 , 𝑦 } } ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) )
29 23 27 28 3bitr4ri ⊢ ( ( { 𝑥 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) ∧ { 𝑥 , 𝑦 } ∈ 𝒫 ( 𝐴 ∪ 𝐵 ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) )
30 21 29 sylib ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) )
31 2 30 sylbi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) )
32 1 31 relssi ⊢ ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 )