Theorem altxpsspw

Description: An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012)

	Ref	Expression
Assertion	altxpsspw	⊢ ( 𝐴 ×× 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elaltxp	⊢ ( 𝑧 ∈ ( 𝐴 ×× 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ )
2		df-altop	⊢ ⟪ 𝑥 , 𝑦 ⟫ = { { 𝑥 } , { 𝑥 , { 𝑦 } } }
3		snssi	⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ⊆ 𝐴 )
4		ssun3	⊢ ( { 𝑥 } ⊆ 𝐴 → { 𝑥 } ⊆ ( 𝐴 ∪ 𝒫 𝐵 ) )
5	3 4	syl	⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ⊆ ( 𝐴 ∪ 𝒫 𝐵 ) )
6	5	adantr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 } ⊆ ( 𝐴 ∪ 𝒫 𝐵 ) )
7		elun1	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐴 ∪ 𝒫 𝐵 ) )
8		snssi	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ⊆ 𝐵 )
9		snex	⊢ { 𝑦 } ∈ V
10	9	elpw	⊢ ( { 𝑦 } ∈ 𝒫 𝐵 ↔ { 𝑦 } ⊆ 𝐵 )
11		elun2	⊢ ( { 𝑦 } ∈ 𝒫 𝐵 → { 𝑦 } ∈ ( 𝐴 ∪ 𝒫 𝐵 ) )
12	10 11	sylbir	⊢ ( { 𝑦 } ⊆ 𝐵 → { 𝑦 } ∈ ( 𝐴 ∪ 𝒫 𝐵 ) )
13	8 12	syl	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ∈ ( 𝐴 ∪ 𝒫 𝐵 ) )
14	7 13	anim12i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐴 ∪ 𝒫 𝐵 ) ∧ { 𝑦 } ∈ ( 𝐴 ∪ 𝒫 𝐵 ) ) )
15		vex	⊢ 𝑥 ∈ V
16	15 9	prss	⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝒫 𝐵 ) ∧ { 𝑦 } ∈ ( 𝐴 ∪ 𝒫 𝐵 ) ) ↔ { 𝑥 , { 𝑦 } } ⊆ ( 𝐴 ∪ 𝒫 𝐵 ) )
17	14 16	sylib	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 , { 𝑦 } } ⊆ ( 𝐴 ∪ 𝒫 𝐵 ) )
18		prex	⊢ { { 𝑥 } , { 𝑥 , { 𝑦 } } } ∈ V
19	18	elpw	⊢ ( { { 𝑥 } , { 𝑥 , { 𝑦 } } } ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) ↔ { { 𝑥 } , { 𝑥 , { 𝑦 } } } ⊆ 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) )
20		snex	⊢ { 𝑥 } ∈ V
21		prex	⊢ { 𝑥 , { 𝑦 } } ∈ V
22	20 21	prsspw	⊢ ( { { 𝑥 } , { 𝑥 , { 𝑦 } } } ⊆ 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) ↔ ( { 𝑥 } ⊆ ( 𝐴 ∪ 𝒫 𝐵 ) ∧ { 𝑥 , { 𝑦 } } ⊆ ( 𝐴 ∪ 𝒫 𝐵 ) ) )
23	19 22	bitri	⊢ ( { { 𝑥 } , { 𝑥 , { 𝑦 } } } ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) ↔ ( { 𝑥 } ⊆ ( 𝐴 ∪ 𝒫 𝐵 ) ∧ { 𝑥 , { 𝑦 } } ⊆ ( 𝐴 ∪ 𝒫 𝐵 ) ) )
24	6 17 23	sylanbrc	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → { { 𝑥 } , { 𝑥 , { 𝑦 } } } ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) )
25	2 24	eqeltrid	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟪ 𝑥 , 𝑦 ⟫ ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) )
26		eleq1a	⊢ ( ⟪ 𝑥 , 𝑦 ⟫ ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) → ( 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ → 𝑧 ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) ) )
27	25 26	syl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ → 𝑧 ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) ) )
28	27	rexlimivv	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ → 𝑧 ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) )
29	1 28	sylbi	⊢ ( 𝑧 ∈ ( 𝐴 ×× 𝐵 ) → 𝑧 ∈ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 ) )
30	29	ssriv	⊢ ( 𝐴 ×× 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝒫 𝐵 )