Step | Hyp | Ref
| Expression |
1 | | relxp 5553 |
. 2
⊢ Rel
(𝐴 × 𝐵) |
2 | | opelxp 5571 |
. . 3
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
3 | | snssi 4706 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ 𝐴) |
4 | | ssun3 4074 |
. . . . . . . 8
⊢ ({𝑥} ⊆ 𝐴 → {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
6 | | snex 5308 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
7 | 6 | elpw 4502 |
. . . . . . 7
⊢ ({𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵) ↔ {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
8 | 5, 7 | sylibr 237 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵)) |
9 | 8 | adantr 484 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵)) |
10 | | df-pr 4529 |
. . . . . . 7
⊢ {𝑥, 𝑦} = ({𝑥} ∪ {𝑦}) |
11 | | snssi 4706 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 → {𝑦} ⊆ 𝐵) |
12 | | ssun4 4075 |
. . . . . . . . . 10
⊢ ({𝑦} ⊆ 𝐵 → {𝑦} ⊆ (𝐴 ∪ 𝐵)) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → {𝑦} ⊆ (𝐴 ∪ 𝐵)) |
14 | 5, 13 | anim12i 616 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} ⊆ (𝐴 ∪ 𝐵) ∧ {𝑦} ⊆ (𝐴 ∪ 𝐵))) |
15 | | unss 4084 |
. . . . . . . 8
⊢ (({𝑥} ⊆ (𝐴 ∪ 𝐵) ∧ {𝑦} ⊆ (𝐴 ∪ 𝐵)) ↔ ({𝑥} ∪ {𝑦}) ⊆ (𝐴 ∪ 𝐵)) |
16 | 14, 15 | sylib 221 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴 ∪ 𝐵)) |
17 | 10, 16 | eqsstrid 3935 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑥, 𝑦} ⊆ (𝐴 ∪ 𝐵)) |
18 | | zfpair2 5307 |
. . . . . . 7
⊢ {𝑥, 𝑦} ∈ V |
19 | 18 | elpw 4502 |
. . . . . 6
⊢ ({𝑥, 𝑦} ∈ 𝒫 (𝐴 ∪ 𝐵) ↔ {𝑥, 𝑦} ⊆ (𝐴 ∪ 𝐵)) |
20 | 17, 19 | sylibr 237 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑥, 𝑦} ∈ 𝒫 (𝐴 ∪ 𝐵)) |
21 | 9, 20 | jca 515 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵) ∧ {𝑥, 𝑦} ∈ 𝒫 (𝐴 ∪ 𝐵))) |
22 | | prex 5309 |
. . . . . 6
⊢ {{𝑥}, {𝑥, 𝑦}} ∈ V |
23 | 22 | elpw 4502 |
. . . . 5
⊢ ({{𝑥}, {𝑥, 𝑦}} ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵) ↔ {{𝑥}, {𝑥, 𝑦}} ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
24 | | vex 3404 |
. . . . . . 7
⊢ 𝑥 ∈ V |
25 | | vex 3404 |
. . . . . . 7
⊢ 𝑦 ∈ V |
26 | 24, 25 | dfop 4768 |
. . . . . 6
⊢
〈𝑥, 𝑦〉 = {{𝑥}, {𝑥, 𝑦}} |
27 | 26 | eleq1i 2824 |
. . . . 5
⊢
(〈𝑥, 𝑦〉 ∈ 𝒫
𝒫 (𝐴 ∪ 𝐵) ↔ {{𝑥}, {𝑥, 𝑦}} ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵)) |
28 | 6, 18 | prss 4718 |
. . . . 5
⊢ (({𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵) ∧ {𝑥, 𝑦} ∈ 𝒫 (𝐴 ∪ 𝐵)) ↔ {{𝑥}, {𝑥, 𝑦}} ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
29 | 23, 27, 28 | 3bitr4ri 307 |
. . . 4
⊢ (({𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵) ∧ {𝑥, 𝑦} ∈ 𝒫 (𝐴 ∪ 𝐵)) ↔ 〈𝑥, 𝑦〉 ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵)) |
30 | 21, 29 | sylib 221 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵)) |
31 | 2, 30 | sylbi 220 |
. 2
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) → 〈𝑥, 𝑦〉 ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵)) |
32 | 1, 31 | relssi 5641 |
1
⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) |