Step | Hyp | Ref
| Expression |
1 | | bdcriota.bd |
. . . . . . . . 9
⊢
BOUNDED 𝜑 |
2 | 1 | ax-bdsb 9942 |
. . . . . . . 8
⊢
BOUNDED [𝑧 / 𝑥]𝜑 |
3 | | ax-bdel 9941 |
. . . . . . . 8
⊢
BOUNDED 𝑡 ∈ 𝑧 |
4 | 2, 3 | ax-bdim 9934 |
. . . . . . 7
⊢
BOUNDED ([𝑧 / 𝑥]𝜑 → 𝑡 ∈ 𝑧) |
5 | 4 | ax-bdal 9938 |
. . . . . 6
⊢
BOUNDED ∀𝑧 ∈ 𝑦 ([𝑧 / 𝑥]𝜑 → 𝑡 ∈ 𝑧) |
6 | | df-ral 2311 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝑦 ([𝑧 / 𝑥]𝜑 → 𝑡 ∈ 𝑧) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ([𝑧 / 𝑥]𝜑 → 𝑡 ∈ 𝑧))) |
7 | | impexp 250 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝑦 ∧ [𝑧 / 𝑥]𝜑) → 𝑡 ∈ 𝑧) ↔ (𝑧 ∈ 𝑦 → ([𝑧 / 𝑥]𝜑 → 𝑡 ∈ 𝑧))) |
8 | 7 | bicomi 123 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑦 → ([𝑧 / 𝑥]𝜑 → 𝑡 ∈ 𝑧)) ↔ ((𝑧 ∈ 𝑦 ∧ [𝑧 / 𝑥]𝜑) → 𝑡 ∈ 𝑧)) |
9 | 8 | albii 1359 |
. . . . . . . . 9
⊢
(∀𝑧(𝑧 ∈ 𝑦 → ([𝑧 / 𝑥]𝜑 → 𝑡 ∈ 𝑧)) ↔ ∀𝑧((𝑧 ∈ 𝑦 ∧ [𝑧 / 𝑥]𝜑) → 𝑡 ∈ 𝑧)) |
10 | 6, 9 | bitri 173 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑦 ([𝑧 / 𝑥]𝜑 → 𝑡 ∈ 𝑧) ↔ ∀𝑧((𝑧 ∈ 𝑦 ∧ [𝑧 / 𝑥]𝜑) → 𝑡 ∈ 𝑧)) |
11 | | sban 1829 |
. . . . . . . . . . . 12
⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝑦 ∧ 𝜑) ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝑦 ∧ [𝑧 / 𝑥]𝜑)) |
12 | | clelsb3 2142 |
. . . . . . . . . . . . 13
⊢ ([𝑧 / 𝑥]𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦) |
13 | 12 | anbi1i 431 |
. . . . . . . . . . . 12
⊢ (([𝑧 / 𝑥]𝑥 ∈ 𝑦 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑧 ∈ 𝑦 ∧ [𝑧 / 𝑥]𝜑)) |
14 | 11, 13 | bitri 173 |
. . . . . . . . . . 11
⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝑦 ∧ 𝜑) ↔ (𝑧 ∈ 𝑦 ∧ [𝑧 / 𝑥]𝜑)) |
15 | 14 | bicomi 123 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑦 ∧ [𝑧 / 𝑥]𝜑) ↔ [𝑧 / 𝑥](𝑥 ∈ 𝑦 ∧ 𝜑)) |
16 | 15 | imbi1i 227 |
. . . . . . . . 9
⊢ (((𝑧 ∈ 𝑦 ∧ [𝑧 / 𝑥]𝜑) → 𝑡 ∈ 𝑧) ↔ ([𝑧 / 𝑥](𝑥 ∈ 𝑦 ∧ 𝜑) → 𝑡 ∈ 𝑧)) |
17 | 16 | albii 1359 |
. . . . . . . 8
⊢
(∀𝑧((𝑧 ∈ 𝑦 ∧ [𝑧 / 𝑥]𝜑) → 𝑡 ∈ 𝑧) ↔ ∀𝑧([𝑧 / 𝑥](𝑥 ∈ 𝑦 ∧ 𝜑) → 𝑡 ∈ 𝑧)) |
18 | 10, 17 | bitri 173 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑦 ([𝑧 / 𝑥]𝜑 → 𝑡 ∈ 𝑧) ↔ ∀𝑧([𝑧 / 𝑥](𝑥 ∈ 𝑦 ∧ 𝜑) → 𝑡 ∈ 𝑧)) |
19 | | df-clab 2027 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝑦 ∧ 𝜑)} ↔ [𝑧 / 𝑥](𝑥 ∈ 𝑦 ∧ 𝜑)) |
20 | 19 | bicomi 123 |
. . . . . . . . 9
⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝑦 ∧ 𝜑) ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝑦 ∧ 𝜑)}) |
21 | 20 | imbi1i 227 |
. . . . . . . 8
⊢ (([𝑧 / 𝑥](𝑥 ∈ 𝑦 ∧ 𝜑) → 𝑡 ∈ 𝑧) ↔ (𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝑦 ∧ 𝜑)} → 𝑡 ∈ 𝑧)) |
22 | 21 | albii 1359 |
. . . . . . 7
⊢
(∀𝑧([𝑧 / 𝑥](𝑥 ∈ 𝑦 ∧ 𝜑) → 𝑡 ∈ 𝑧) ↔ ∀𝑧(𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝑦 ∧ 𝜑)} → 𝑡 ∈ 𝑧)) |
23 | 18, 22 | bitri 173 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑦 ([𝑧 / 𝑥]𝜑 → 𝑡 ∈ 𝑧) ↔ ∀𝑧(𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝑦 ∧ 𝜑)} → 𝑡 ∈ 𝑧)) |
24 | 5, 23 | bd0 9944 |
. . . . 5
⊢
BOUNDED ∀𝑧(𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝑦 ∧ 𝜑)} → 𝑡 ∈ 𝑧) |
25 | 24 | bdcab 9969 |
. . . 4
⊢
BOUNDED {𝑡 ∣ ∀𝑧(𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝑦 ∧ 𝜑)} → 𝑡 ∈ 𝑧)} |
26 | | df-int 3616 |
. . . 4
⊢ ∩ {𝑥
∣ (𝑥 ∈ 𝑦 ∧ 𝜑)} = {𝑡 ∣ ∀𝑧(𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝑦 ∧ 𝜑)} → 𝑡 ∈ 𝑧)} |
27 | 25, 26 | bdceqir 9964 |
. . 3
⊢
BOUNDED ∩ {𝑥 ∣ (𝑥 ∈ 𝑦 ∧ 𝜑)} |
28 | | bdcriota.ex |
. . . . 5
⊢
∃!𝑥 ∈
𝑦 𝜑 |
29 | | df-reu 2313 |
. . . . 5
⊢
(∃!𝑥 ∈
𝑦 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)) |
30 | 28, 29 | mpbi 133 |
. . . 4
⊢
∃!𝑥(𝑥 ∈ 𝑦 ∧ 𝜑) |
31 | | iotaint 4880 |
. . . 4
⊢
(∃!𝑥(𝑥 ∈ 𝑦 ∧ 𝜑) → (℩𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)) = ∩ {𝑥 ∣ (𝑥 ∈ 𝑦 ∧ 𝜑)}) |
32 | 30, 31 | ax-mp 7 |
. . 3
⊢
(℩𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)) = ∩ {𝑥 ∣ (𝑥 ∈ 𝑦 ∧ 𝜑)} |
33 | 27, 32 | bdceqir 9964 |
. 2
⊢
BOUNDED (℩𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)) |
34 | | df-riota 5468 |
. 2
⊢
(℩𝑥
∈ 𝑦 𝜑) = (℩𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)) |
35 | 33, 34 | bdceqir 9964 |
1
⊢
BOUNDED (℩𝑥 ∈ 𝑦 𝜑) |