Step | Hyp | Ref
| Expression |
1 | | nfv 1421 |
. . 3
⊢
Ⅎ𝑐(𝑢 = 𝑎 ∧ 𝑣 = 𝑏) |
2 | | nfv 1421 |
. . . 4
⊢
Ⅎ𝑧(𝑢 = 𝑎 ∧ 𝑣 = 𝑏) |
3 | | simpl 102 |
. . . . . 6
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → 𝑢 = 𝑎) |
4 | | rexeq 2506 |
. . . . . . 7
⊢ (𝑣 = 𝑏 → (∃𝑦 ∈ 𝑣 𝜑 ↔ ∃𝑦 ∈ 𝑏 𝜑)) |
5 | 4 | adantl 262 |
. . . . . 6
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑦 ∈ 𝑣 𝜑 ↔ ∃𝑦 ∈ 𝑏 𝜑)) |
6 | 3, 5 | raleqbidv 2517 |
. . . . 5
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 ↔ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑)) |
7 | | nfv 1421 |
. . . . . 6
⊢
Ⅎ𝑑(𝑢 = 𝑎 ∧ 𝑣 = 𝑏) |
8 | | nfv 1421 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑢 = 𝑎 ∧ 𝑣 = 𝑏) |
9 | | rexeq 2506 |
. . . . . . . . 9
⊢ (𝑢 = 𝑎 → (∃𝑥 ∈ 𝑢 𝜑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) |
10 | 9 | adantr 261 |
. . . . . . . 8
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑥 ∈ 𝑢 𝜑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) |
11 | 10 | bibi2d 221 |
. . . . . . 7
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → ((𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑) ↔ (𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))) |
12 | 8, 11 | albid 1506 |
. . . . . 6
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))) |
13 | 7, 12 | rexbid 2325 |
. . . . 5
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑) ↔ ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))) |
14 | 6, 13 | imbi12d 223 |
. . . 4
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) ↔ (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)))) |
15 | 2, 14 | albid 1506 |
. . 3
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) ↔ ∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)))) |
16 | 1, 15 | exbid 1507 |
. 2
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) ↔ ∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)))) |
17 | | ax-sscoll 10112 |
. . . 4
⊢
∀𝑢∀𝑣∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) |
18 | 17 | spi 1429 |
. . 3
⊢
∀𝑣∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) |
19 | 18 | spi 1429 |
. 2
⊢
∃𝑐∀𝑧(∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝑣 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑢 𝜑)) |
20 | 16, 19 | ch2varv 9908 |
1
⊢
∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) |