Step | Hyp | Ref
| Expression |
1 | | bdvsn 14596 |
. . . 4
⊢
BOUNDED 𝑧 = {𝑥} |
2 | | bdcpr 14593 |
. . . . . . 7
⊢
BOUNDED {𝑥, 𝑦} |
3 | 2 | bdss 14586 |
. . . . . 6
⊢
BOUNDED 𝑧 ⊆ {𝑥, 𝑦} |
4 | | ax-bdel 14543 |
. . . . . . . 8
⊢
BOUNDED 𝑥 ∈ 𝑧 |
5 | | ax-bdel 14543 |
. . . . . . . 8
⊢
BOUNDED 𝑦 ∈ 𝑧 |
6 | 4, 5 | ax-bdan 14537 |
. . . . . . 7
⊢
BOUNDED (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧) |
7 | | vex 2740 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
8 | 7 | prid1 3698 |
. . . . . . . . . 10
⊢ 𝑥 ∈ {𝑥, 𝑦} |
9 | | ssel 3149 |
. . . . . . . . . 10
⊢ ({𝑥, 𝑦} ⊆ 𝑧 → (𝑥 ∈ {𝑥, 𝑦} → 𝑥 ∈ 𝑧)) |
10 | 8, 9 | mpi 15 |
. . . . . . . . 9
⊢ ({𝑥, 𝑦} ⊆ 𝑧 → 𝑥 ∈ 𝑧) |
11 | | vex 2740 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
12 | 11 | prid2 3699 |
. . . . . . . . . 10
⊢ 𝑦 ∈ {𝑥, 𝑦} |
13 | | ssel 3149 |
. . . . . . . . . 10
⊢ ({𝑥, 𝑦} ⊆ 𝑧 → (𝑦 ∈ {𝑥, 𝑦} → 𝑦 ∈ 𝑧)) |
14 | 12, 13 | mpi 15 |
. . . . . . . . 9
⊢ ({𝑥, 𝑦} ⊆ 𝑧 → 𝑦 ∈ 𝑧) |
15 | 10, 14 | jca 306 |
. . . . . . . 8
⊢ ({𝑥, 𝑦} ⊆ 𝑧 → (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧)) |
16 | | prssi 3750 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧) → {𝑥, 𝑦} ⊆ 𝑧) |
17 | 15, 16 | impbii 126 |
. . . . . . 7
⊢ ({𝑥, 𝑦} ⊆ 𝑧 ↔ (𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧)) |
18 | 6, 17 | bd0r 14547 |
. . . . . 6
⊢
BOUNDED {𝑥, 𝑦} ⊆ 𝑧 |
19 | 3, 18 | ax-bdan 14537 |
. . . . 5
⊢
BOUNDED (𝑧 ⊆ {𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝑧) |
20 | | eqss 3170 |
. . . . 5
⊢ (𝑧 = {𝑥, 𝑦} ↔ (𝑧 ⊆ {𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝑧)) |
21 | 19, 20 | bd0r 14547 |
. . . 4
⊢
BOUNDED 𝑧 = {𝑥, 𝑦} |
22 | 1, 21 | ax-bdor 14538 |
. . 3
⊢
BOUNDED (𝑧 = {𝑥} ∨ 𝑧 = {𝑥, 𝑦}) |
23 | | vex 2740 |
. . . 4
⊢ 𝑧 ∈ V |
24 | 23, 7, 11 | elop 4231 |
. . 3
⊢ (𝑧 ∈ ⟨𝑥, 𝑦⟩ ↔ (𝑧 = {𝑥} ∨ 𝑧 = {𝑥, 𝑦})) |
25 | 22, 24 | bd0r 14547 |
. 2
⊢
BOUNDED 𝑧 ∈ ⟨𝑥, 𝑦⟩ |
26 | 25 | bdelir 14569 |
1
⊢
BOUNDED ⟨𝑥, 𝑦⟩ |