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) |