Theorem xpsspw 4373

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 4284	. . . 4 ⊢ (z ∈ (A × B) → ∃x∃y(z = ⟨x, y⟩ ∧ (x ∈ A ∧ y ∈ B)))
2		vex 2534	. . . . . . . 8 ⊢ x ∈ V
3		vex 2534	. . . . . . . 8 ⊢ y ∈ V
4	2, 3	dfop 3518	. . . . . . 7 ⊢ ⟨x, y⟩ = {{x}, {x, y}}
5		snssi 3478	. . . . . . . . . . . . 13 ⊢ (x ∈ A → {x} ⊆ A)
6		ssun3 3081	. . . . . . . . . . . . 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 2939	. . . . . . . . . . 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 3353	. . . . . . . . . . . 12 ⊢ {x, y} = ({x} ∪ {y})
12		snssi 3478	. . . . . . . . . . . . . . 15 ⊢ (y ∈ B → {y} ⊆ B)
13		ssun4 3082	. . . . . . . . . . . . . . 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 3090	. . . . . . . . . . . . 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 2962	. . . . . . . . . . 11 ⊢ ((x ∈ A ∧ y ∈ B) → {x, y} ⊆ (A ∪ B))
19		sseq1 2939	. . . . . . . . . . 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 624	. . . . . . . . 9 ⊢ ((x ∈ A ∧ y ∈ B) → ((z = {x} ∨ z = {x, y}) → z ⊆ (A ∪ B)))
22		vex 2534	. . . . . . . . . 10 ⊢ z ∈ V
23	22	elpr 3364	. . . . . . . . 9 ⊢ (z ∈ {{x}, {x, y}} ↔ (z = {x} ∨ z = {x, y}))
24	22	elpw 3336	. . . . . . . . 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 2924	. . . . . . 7 ⊢ ((x ∈ A ∧ y ∈ B) → {{x}, {x, y}} ⊆ 𝒫 (A ∪ B))
27	4, 26	syl5eqss 2962	. . . . . 6 ⊢ ((x ∈ A ∧ y ∈ B) → ⟨x, y⟩ ⊆ 𝒫 (A ∪ B))
28		sseq1 2939	. . . . . . 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 1754	. . . 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 3336	. . 3 ⊢ (z ∈ 𝒫 𝒫 (A ∪ B) ↔ z ⊆ 𝒫 (A ∪ B))
34	32, 33	sylibr 137	. 2 ⊢ (z ∈ (A × B) → z ∈ 𝒫 𝒫 (A ∪ B))
35	34	ssriv 2922	1 ⊢ (A × B) ⊆ 𝒫 𝒫 (A ∪ B)

Syntax hints:   ∧ wa 97   ∨ wo 616   = wceq 1226  ∃wex 1358   ∈ wcel 1370   ∪ cun 2888   ⊆ wss 2890  𝒫 cpw 3330  {csn 3346  {cpr 3347  ⟨cop 3349   × cxp 4266

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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-opab 3789  df-xp 4274

This theorem is referenced by:  unixpss  4374  xpexg  4375