Step | Hyp | Ref
| Expression |
1 | | elxpi 4625 |
. . . 4
⊢ (𝑧 ∈ (𝐴 × 𝐵) → ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
2 | | vex 2733 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
3 | | vex 2733 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
4 | 2, 3 | dfop 3762 |
. . . . . . 7
⊢
〈𝑥, 𝑦〉 = {{𝑥}, {𝑥, 𝑦}} |
5 | | snssi 3722 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ 𝐴) |
6 | | ssun3 3292 |
. . . . . . . . . . . . 13
⊢ ({𝑥} ⊆ 𝐴 → {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
7 | 5, 6 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
8 | 7 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
9 | | sseq1 3170 |
. . . . . . . . . . 11
⊢ (𝑧 = {𝑥} → (𝑧 ⊆ (𝐴 ∪ 𝐵) ↔ {𝑥} ⊆ (𝐴 ∪ 𝐵))) |
10 | 8, 9 | syl5ibrcom 156 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 = {𝑥} → 𝑧 ⊆ (𝐴 ∪ 𝐵))) |
11 | | df-pr 3588 |
. . . . . . . . . . . 12
⊢ {𝑥, 𝑦} = ({𝑥} ∪ {𝑦}) |
12 | | snssi 3722 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐵 → {𝑦} ⊆ 𝐵) |
13 | | ssun4 3293 |
. . . . . . . . . . . . . . 15
⊢ ({𝑦} ⊆ 𝐵 → {𝑦} ⊆ (𝐴 ∪ 𝐵)) |
14 | 12, 13 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐵 → {𝑦} ⊆ (𝐴 ∪ 𝐵)) |
15 | 7, 14 | anim12i 336 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} ⊆ (𝐴 ∪ 𝐵) ∧ {𝑦} ⊆ (𝐴 ∪ 𝐵))) |
16 | | unss 3301 |
. . . . . . . . . . . . 13
⊢ (({𝑥} ⊆ (𝐴 ∪ 𝐵) ∧ {𝑦} ⊆ (𝐴 ∪ 𝐵)) ↔ ({𝑥} ∪ {𝑦}) ⊆ (𝐴 ∪ 𝐵)) |
17 | 15, 16 | sylib 121 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴 ∪ 𝐵)) |
18 | 11, 17 | eqsstrid 3193 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑥, 𝑦} ⊆ (𝐴 ∪ 𝐵)) |
19 | | sseq1 3170 |
. . . . . . . . . . 11
⊢ (𝑧 = {𝑥, 𝑦} → (𝑧 ⊆ (𝐴 ∪ 𝐵) ↔ {𝑥, 𝑦} ⊆ (𝐴 ∪ 𝐵))) |
20 | 18, 19 | syl5ibrcom 156 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 = {𝑥, 𝑦} → 𝑧 ⊆ (𝐴 ∪ 𝐵))) |
21 | 10, 20 | jaod 712 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ((𝑧 = {𝑥} ∨ 𝑧 = {𝑥, 𝑦}) → 𝑧 ⊆ (𝐴 ∪ 𝐵))) |
22 | | vex 2733 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
23 | 22 | elpr 3602 |
. . . . . . . . 9
⊢ (𝑧 ∈ {{𝑥}, {𝑥, 𝑦}} ↔ (𝑧 = {𝑥} ∨ 𝑧 = {𝑥, 𝑦})) |
24 | 22 | elpw 3570 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝒫 (𝐴 ∪ 𝐵) ↔ 𝑧 ⊆ (𝐴 ∪ 𝐵)) |
25 | 21, 23, 24 | 3imtr4g 204 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ {{𝑥}, {𝑥, 𝑦}} → 𝑧 ∈ 𝒫 (𝐴 ∪ 𝐵))) |
26 | 25 | ssrdv 3153 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {{𝑥}, {𝑥, 𝑦}} ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
27 | 4, 26 | eqsstrid 3193 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
28 | | sseq1 3170 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵) ↔ 〈𝑥, 𝑦〉 ⊆ 𝒫 (𝐴 ∪ 𝐵))) |
29 | 28 | biimpar 295 |
. . . . . 6
⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ⊆ 𝒫 (𝐴 ∪ 𝐵)) → 𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
30 | 27, 29 | sylan2 284 |
. . . . 5
⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
31 | 30 | exlimivv 1889 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
32 | 1, 31 | syl 14 |
. . 3
⊢ (𝑧 ∈ (𝐴 × 𝐵) → 𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
33 | 22 | elpw 3570 |
. . 3
⊢ (𝑧 ∈ 𝒫 𝒫
(𝐴 ∪ 𝐵) ↔ 𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
34 | 32, 33 | sylibr 133 |
. 2
⊢ (𝑧 ∈ (𝐴 × 𝐵) → 𝑧 ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵)) |
35 | 34 | ssriv 3151 |
1
⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) |