Step | Hyp | Ref
| Expression |
1 | | elxpi 4643 |
. . . 4
⊢ (𝑧 ∈ (𝐴 × 𝐵) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
2 | | vex 2741 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
3 | | vex 2741 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
4 | 2, 3 | dfop 3778 |
. . . . . . 7
⊢
⟨𝑥, 𝑦⟩ = {{𝑥}, {𝑥, 𝑦}} |
5 | | snssi 3737 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ 𝐴) |
6 | | ssun3 3301 |
. . . . . . . . . . . . 13
⊢ ({𝑥} ⊆ 𝐴 → {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
7 | 5, 6 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
8 | 7 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑥} ⊆ (𝐴 ∪ 𝐵)) |
9 | | sseq1 3179 |
. . . . . . . . . . 11
⊢ (𝑧 = {𝑥} → (𝑧 ⊆ (𝐴 ∪ 𝐵) ↔ {𝑥} ⊆ (𝐴 ∪ 𝐵))) |
10 | 8, 9 | syl5ibrcom 157 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 = {𝑥} → 𝑧 ⊆ (𝐴 ∪ 𝐵))) |
11 | | df-pr 3600 |
. . . . . . . . . . . 12
⊢ {𝑥, 𝑦} = ({𝑥} ∪ {𝑦}) |
12 | | snssi 3737 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐵 → {𝑦} ⊆ 𝐵) |
13 | | ssun4 3302 |
. . . . . . . . . . . . . . 15
⊢ ({𝑦} ⊆ 𝐵 → {𝑦} ⊆ (𝐴 ∪ 𝐵)) |
14 | 12, 13 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐵 → {𝑦} ⊆ (𝐴 ∪ 𝐵)) |
15 | 7, 14 | anim12i 338 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} ⊆ (𝐴 ∪ 𝐵) ∧ {𝑦} ⊆ (𝐴 ∪ 𝐵))) |
16 | | unss 3310 |
. . . . . . . . . . . . 13
⊢ (({𝑥} ⊆ (𝐴 ∪ 𝐵) ∧ {𝑦} ⊆ (𝐴 ∪ 𝐵)) ↔ ({𝑥} ∪ {𝑦}) ⊆ (𝐴 ∪ 𝐵)) |
17 | 15, 16 | sylib 122 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} ∪ {𝑦}) ⊆ (𝐴 ∪ 𝐵)) |
18 | 11, 17 | eqsstrid 3202 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑥, 𝑦} ⊆ (𝐴 ∪ 𝐵)) |
19 | | sseq1 3179 |
. . . . . . . . . . 11
⊢ (𝑧 = {𝑥, 𝑦} → (𝑧 ⊆ (𝐴 ∪ 𝐵) ↔ {𝑥, 𝑦} ⊆ (𝐴 ∪ 𝐵))) |
20 | 18, 19 | syl5ibrcom 157 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 = {𝑥, 𝑦} → 𝑧 ⊆ (𝐴 ∪ 𝐵))) |
21 | 10, 20 | jaod 717 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ((𝑧 = {𝑥} ∨ 𝑧 = {𝑥, 𝑦}) → 𝑧 ⊆ (𝐴 ∪ 𝐵))) |
22 | | vex 2741 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
23 | 22 | elpr 3614 |
. . . . . . . . 9
⊢ (𝑧 ∈ {{𝑥}, {𝑥, 𝑦}} ↔ (𝑧 = {𝑥} ∨ 𝑧 = {𝑥, 𝑦})) |
24 | 22 | elpw 3582 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝒫 (𝐴 ∪ 𝐵) ↔ 𝑧 ⊆ (𝐴 ∪ 𝐵)) |
25 | 21, 23, 24 | 3imtr4g 205 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ {{𝑥}, {𝑥, 𝑦}} → 𝑧 ∈ 𝒫 (𝐴 ∪ 𝐵))) |
26 | 25 | ssrdv 3162 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {{𝑥}, {𝑥, 𝑦}} ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
27 | 4, 26 | eqsstrid 3202 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⟨𝑥, 𝑦⟩ ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
28 | | sseq1 3179 |
. . . . . . 7
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵) ↔ ⟨𝑥, 𝑦⟩ ⊆ 𝒫 (𝐴 ∪ 𝐵))) |
29 | 28 | biimpar 297 |
. . . . . 6
⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ⊆ 𝒫 (𝐴 ∪ 𝐵)) → 𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
30 | 27, 29 | sylan2 286 |
. . . . 5
⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
31 | 30 | exlimivv 1896 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
32 | 1, 31 | syl 14 |
. . 3
⊢ (𝑧 ∈ (𝐴 × 𝐵) → 𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
33 | 22 | elpw 3582 |
. . 3
⊢ (𝑧 ∈ 𝒫 𝒫
(𝐴 ∪ 𝐵) ↔ 𝑧 ⊆ 𝒫 (𝐴 ∪ 𝐵)) |
34 | 32, 33 | sylibr 134 |
. 2
⊢ (𝑧 ∈ (𝐴 × 𝐵) → 𝑧 ∈ 𝒫 𝒫 (𝐴 ∪ 𝐵)) |
35 | 34 | ssriv 3160 |
1
⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) |