Theorem xpsspw 4393

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

Assertion

Ref	Expression
xpsspw	⊢ (A × B) ⊆ 𝒫 𝒫 (A ∪ B)

Proof of Theorem xpsspw

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxpi 4304	. . . 4 ⊢ (z ∈ (A × B) → ∃x∃y(z = ⟨x, y⟩ ∧ (x ∈ A ∧ y ∈ B)))
2		vex 2554	. . . . . . . 8 ⊢ x ∈ V
3		vex 2554	. . . . . . . 8 ⊢ y ∈ V
4	2, 3	dfop 3539	. . . . . . 7 ⊢ ⟨x, y⟩ = {{x}, {x, y}}
5		snssi 3499	. . . . . . . . . . . . 13 ⊢ (x ∈ A → {x} ⊆ A)
6		ssun3 3102	. . . . . . . . . . . . 13 ⊢ ({x} ⊆ A → {x} ⊆ (A ∪ B))
7	5, 6	syl 14	. . . . . . . . . . . 12 ⊢ (x ∈ A → {x} ⊆ (A ∪ B))
8	7	adantr 261	. . . . . . . . . . 11 ⊢ ((x ∈ A ∧ y ∈ B) → {x} ⊆ (A ∪ B))
9		sseq1 2960	. . . . . . . . . . 11 ⊢ (z = {x} → (z ⊆ (A ∪ B) ↔ {x} ⊆ (A ∪ B)))
10	8, 9	syl5ibrcom 146	. . . . . . . . . 10 ⊢ ((x ∈ A ∧ y ∈ B) → (z = {x} → z ⊆ (A ∪ B)))
11		df-pr 3374	. . . . . . . . . . . 12 ⊢ {x, y} = ({x} ∪ {y})
12		snssi 3499	. . . . . . . . . . . . . . 15 ⊢ (y ∈ B → {y} ⊆ B)
13		ssun4 3103	. . . . . . . . . . . . . . 15 ⊢ ({y} ⊆ B → {y} ⊆ (A ∪ B))
14	12, 13	syl 14	. . . . . . . . . . . . . 14 ⊢ (y ∈ B → {y} ⊆ (A ∪ B))
15	7, 14	anim12i 321	. . . . . . . . . . . . 13 ⊢ ((x ∈ A ∧ y ∈ B) → ({x} ⊆ (A ∪ B) ∧ {y} ⊆ (A ∪ B)))
16		unss 3111	. . . . . . . . . . . . 13 ⊢ (({x} ⊆ (A ∪ B) ∧ {y} ⊆ (A ∪ B)) ↔ ({x} ∪ {y}) ⊆ (A ∪ B))
17	15, 16	sylib 127	. . . . . . . . . . . 12 ⊢ ((x ∈ A ∧ y ∈ B) → ({x} ∪ {y}) ⊆ (A ∪ B))
18	11, 17	syl5eqss 2983	. . . . . . . . . . 11 ⊢ ((x ∈ A ∧ y ∈ B) → {x, y} ⊆ (A ∪ B))
19		sseq1 2960	. . . . . . . . . . 11 ⊢ (z = {x, y} → (z ⊆ (A ∪ B) ↔ {x, y} ⊆ (A ∪ B)))
20	18, 19	syl5ibrcom 146	. . . . . . . . . 10 ⊢ ((x ∈ A ∧ y ∈ B) → (z = {x, y} → z ⊆ (A ∪ B)))
21	10, 20	jaod 636	. . . . . . . . 9 ⊢ ((x ∈ A ∧ y ∈ B) → ((z = {x} ∨ z = {x, y}) → z ⊆ (A ∪ B)))
22		vex 2554	. . . . . . . . . 10 ⊢ z ∈ V
23	22	elpr 3385	. . . . . . . . 9 ⊢ (z ∈ {{x}, {x, y}} ↔ (z = {x} ∨ z = {x, y}))
24	22	elpw 3357	. . . . . . . . 9 ⊢ (z ∈ 𝒫 (A ∪ B) ↔ z ⊆ (A ∪ B))
25	21, 23, 24	3imtr4g 194	. . . . . . . 8 ⊢ ((x ∈ A ∧ y ∈ B) → (z ∈ {{x}, {x, y}} → z ∈ 𝒫 (A ∪ B)))
26	25	ssrdv 2945	. . . . . . 7 ⊢ ((x ∈ A ∧ y ∈ B) → {{x}, {x, y}} ⊆ 𝒫 (A ∪ B))
27	4, 26	syl5eqss 2983	. . . . . 6 ⊢ ((x ∈ A ∧ y ∈ B) → ⟨x, y⟩ ⊆ 𝒫 (A ∪ B))
28		sseq1 2960	. . . . . . 7 ⊢ (z = ⟨x, y⟩ → (z ⊆ 𝒫 (A ∪ B) ↔ ⟨x, y⟩ ⊆ 𝒫 (A ∪ B)))
29	28	biimpar 281	. . . . . 6 ⊢ ((z = ⟨x, y⟩ ∧ ⟨x, y⟩ ⊆ 𝒫 (A ∪ B)) → z ⊆ 𝒫 (A ∪ B))
30	27, 29	sylan2 270	. . . . 5 ⊢ ((z = ⟨x, y⟩ ∧ (x ∈ A ∧ y ∈ B)) → z ⊆ 𝒫 (A ∪ B))
31	30	exlimivv 1773	. . . 4 ⊢ (∃x∃y(z = ⟨x, y⟩ ∧ (x ∈ A ∧ y ∈ B)) → z ⊆ 𝒫 (A ∪ B))
32	1, 31	syl 14	. . 3 ⊢ (z ∈ (A × B) → z ⊆ 𝒫 (A ∪ B))
33	22	elpw 3357	. . 3 ⊢ (z ∈ 𝒫 𝒫 (A ∪ B) ↔ z ⊆ 𝒫 (A ∪ B))
34	32, 33	sylibr 137	. 2 ⊢ (z ∈ (A × B) → z ∈ 𝒫 𝒫 (A ∪ B))
35	34	ssriv 2943	1 ⊢ (A × B) ⊆ 𝒫 𝒫 (A ∪ B)

Syntax hints:   ∧ wa 97   ∨ wo 628   = wceq 1242  ∃wex 1378   ∈ wcel 1390   ∪ cun 2909   ⊆ wss 2911  𝒫 cpw 3351  {csn 3367  {cpr 3368  ⟨cop 3370   × cxp 4286

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810  df-xp 4294

This theorem is referenced by:  unixpss  4394  xpexg  4395