| Step | Hyp | Ref
| Expression |
| 1 | | relxp 5703 |
. 2
⊢ Rel
(𝐴 × 𝐵) |
| 2 | | opelxp 5721 |
. . 3
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 3 | | snssi 4808 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ 𝐴) |
| 4 | | ssun3 4180 |
. . . . . . . 8
⊢ ({𝑥} ⊆ 𝐴 → {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
| 5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
| 6 | | vsnex 5434 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
| 7 | 6 | elpw 4604 |
. . . . . . 7
⊢ ({𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵) ↔ {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
| 8 | 5, 7 | sylibr 234 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵)) |
| 9 | 8 | adantr 480 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵)) |
| 10 | | df-pr 4629 |
. . . . . . 7
⊢ {𝑥, 𝑦} = ({𝑥} ∪ {𝑦}) |
| 11 | | snssi 4808 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 → {𝑦} ⊆ 𝐵) |
| 12 | | ssun4 4181 |
. . . . . . . . . 10
⊢ ({𝑦} ⊆ 𝐵 → {𝑦} ⊆ (𝐴 ∪ 𝐵)) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → {𝑦} ⊆ (𝐴 ∪ 𝐵)) |
| 14 | 5, 13 | anim12i 613 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} ⊆ (𝐴 ∪ 𝐵) ∧ {𝑦} ⊆ (𝐴 ∪ 𝐵))) |
| 15 | | unss 4190 |
. . . . . . . 8
⊢ (({𝑥} ⊆ (𝐴 ∪ 𝐵) ∧ {𝑦} ⊆ (𝐴 ∪ 𝐵)) ↔ ({𝑥} ∪ {𝑦}) ⊆ (𝐴 ∪ 𝐵)) |
| 16 | 14, 15 | sylib 218 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴 ∪ 𝐵)) |
| 17 | 10, 16 | eqsstrid 4022 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑥, 𝑦} ⊆ (𝐴 ∪ 𝐵)) |
| 18 | | zfpair2 5433 |
. . . . . . 7
⊢ {𝑥, 𝑦} ∈ V |
| 19 | 18 | elpw 4604 |
. . . . . 6
⊢ ({𝑥, 𝑦} ∈ 𝒫 (𝐴 ∪ 𝐵) ↔ {𝑥, 𝑦} ⊆ (𝐴 ∪ 𝐵)) |
| 20 | 17, 19 | sylibr 234 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑥, 𝑦} ∈ 𝒫 (𝐴 ∪ 𝐵)) |
| 21 | 9, 20 | jca 511 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵) ∧ {𝑥, 𝑦} ∈ 𝒫 (𝐴 ∪ 𝐵))) |
| 22 | | prex 5437 |
. . . . . 6
⊢ {{𝑥}, {𝑥, 𝑦}} ∈ V |
| 23 | 22 | elpw 4604 |
. . . . 5
⊢ ({{𝑥}, {𝑥, 𝑦}} ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵) ↔ {{𝑥}, {𝑥, 𝑦}} ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
| 24 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 25 | | vex 3484 |
. . . . . . 7
⊢ 𝑦 ∈ V |
| 26 | 24, 25 | dfop 4872 |
. . . . . 6
⊢
〈𝑥, 𝑦〉 = {{𝑥}, {𝑥, 𝑦}} |
| 27 | 26 | eleq1i 2832 |
. . . . 5
⊢
(〈𝑥, 𝑦〉 ∈ 𝒫
𝒫 (𝐴 ∪ 𝐵) ↔ {{𝑥}, {𝑥, 𝑦}} ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵)) |
| 28 | 6, 18 | prss 4820 |
. . . . 5
⊢ (({𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵) ∧ {𝑥, 𝑦} ∈ 𝒫 (𝐴 ∪ 𝐵)) ↔ {{𝑥}, {𝑥, 𝑦}} ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
| 29 | 23, 27, 28 | 3bitr4ri 304 |
. . . 4
⊢ (({𝑥} ∈ 𝒫 (𝐴 ∪ 𝐵) ∧ {𝑥, 𝑦} ∈ 𝒫 (𝐴 ∪ 𝐵)) ↔ 〈𝑥, 𝑦〉 ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵)) |
| 30 | 21, 29 | sylib 218 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵)) |
| 31 | 2, 30 | sylbi 217 |
. 2
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) → 〈𝑥, 𝑦〉 ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵)) |
| 32 | 1, 31 | relssi 5797 |
1
⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) |