Step | Hyp | Ref
| Expression |
1 | | nfv 1461 |
. . 3
⊢
Ⅎ𝑐(𝑢 = 𝑎 ∧ 𝑣 = 𝑏) |
2 | | nfv 1461 |
. . . 4
⊢
Ⅎ𝑧(𝑢 = 𝑎 ∧ 𝑣 = 𝑏) |
3 | | simpl 107 |
. . . . . 6
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → 𝑢 = 𝑎) |
4 | | rexeq 2550 |
. . . . . . 7
⊢ (𝑣 = 𝑏 → (∃𝑦 ∈ 𝑣 𝜑 ↔ ∃𝑦 ∈ 𝑏 𝜑)) |
5 | 4 | adantl 271 |
. . . . . 6
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑦 ∈ 𝑣 𝜑 ↔ ∃𝑦 ∈ 𝑏 𝜑)) |
6 | 3, 5 | raleqbidv 2561 |
. . . . 5
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 ↔ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑)) |
7 | | nfv 1461 |
. . . . . 6
⊢
Ⅎ𝑑(𝑢 = 𝑎 ∧ 𝑣 = 𝑏) |
8 | | nfv 1461 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑢 = 𝑎 ∧ 𝑣 = 𝑏) |
9 | | rexeq 2550 |
. . . . . . . . 9
⊢ (𝑢 = 𝑎 → (∃𝑥 ∈ 𝑢 𝜑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) |
10 | 9 | adantr 270 |
. . . . . . . 8
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑥 ∈ 𝑢 𝜑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) |
11 | 10 | bibi2d 230 |
. . . . . . 7
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → ((𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑) ↔ (𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))) |
12 | 8, 11 | albid 1546 |
. . . . . 6
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))) |
13 | 7, 12 | rexbid 2367 |
. . . . 5
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑) ↔ ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))) |
14 | 6, 13 | imbi12d 232 |
. . . 4
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) ↔ (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)))) |
15 | 2, 14 | albid 1546 |
. . 3
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) ↔ ∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)))) |
16 | 1, 15 | exbid 1547 |
. 2
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) ↔ ∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)))) |
17 | | ax-sscoll 10782 |
. . . 4
⊢
∀𝑢∀𝑣∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) |
18 | 17 | spi 1469 |
. . 3
⊢
∀𝑣∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) |
19 | 18 | spi 1469 |
. 2
⊢
∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) |
20 | 16, 19 | ch2varv 10579 |
1
⊢
∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) |