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		snex	⊢ { 𝑥 } ∈ 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	⊢ ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 )