Step | Hyp | Ref
| Expression |
1 | | rngop.1 |
. . . . 5
⊢ 𝐹 = (x ∈ A, y ∈ B ↦
𝐶) |
2 | 1 | rnmpt2 5553 |
. . . 4
⊢ ran 𝐹 = {w ∣ ∃x ∈ A ∃y ∈ B w = 𝐶} |
3 | 2 | raleqi 2503 |
. . 3
⊢ (∀z ∈ ran 𝐹φ
↔ ∀z ∈ {w ∣ ∃x ∈ A ∃y ∈ B w = 𝐶}φ) |
4 | | eqeq1 2043 |
. . . . 5
⊢ (w = z →
(w = 𝐶 ↔ z = 𝐶)) |
5 | 4 | 2rexbidv 2343 |
. . . 4
⊢ (w = z →
(∃x
∈ A ∃y ∈ B w = 𝐶 ↔ ∃x ∈ A ∃y ∈ B z = 𝐶)) |
6 | 5 | ralab 2695 |
. . 3
⊢ (∀z ∈ {w ∣
∃x ∈ A ∃y ∈ B w = 𝐶}φ
↔ ∀z(∃x ∈ A ∃y ∈ B z = 𝐶 → φ)) |
7 | | ralcom4 2570 |
. . . 4
⊢ (∀x ∈ A ∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀z∀x ∈ A (∃y ∈ B z = 𝐶 → φ)) |
8 | | r19.23v 2419 |
. . . . 5
⊢ (∀x ∈ A (∃y ∈ B z = 𝐶 → φ) ↔ (∃x ∈ A ∃y ∈ B z = 𝐶 → φ)) |
9 | 8 | albii 1356 |
. . . 4
⊢ (∀z∀x ∈ A (∃y ∈ B z = 𝐶 → φ) ↔ ∀z(∃x ∈ A ∃y ∈ B z = 𝐶 → φ)) |
10 | 7, 9 | bitr2i 174 |
. . 3
⊢ (∀z(∃x ∈ A ∃y ∈ B z = 𝐶 → φ) ↔ ∀x ∈ A ∀z(∃y ∈ B z = 𝐶 → φ)) |
11 | 3, 6, 10 | 3bitri 195 |
. 2
⊢ (∀z ∈ ran 𝐹φ
↔ ∀x ∈ A ∀z(∃y ∈ B z = 𝐶 → φ)) |
12 | | ralcom4 2570 |
. . . . . 6
⊢ (∀y ∈ B ∀z(z = 𝐶 → φ) ↔ ∀z∀y ∈ B (z = 𝐶 → φ)) |
13 | | r19.23v 2419 |
. . . . . . 7
⊢ (∀y ∈ B (z = 𝐶 → φ) ↔ (∃y ∈ B z = 𝐶 → φ)) |
14 | 13 | albii 1356 |
. . . . . 6
⊢ (∀z∀y ∈ B (z = 𝐶 → φ) ↔ ∀z(∃y ∈ B z = 𝐶 → φ)) |
15 | 12, 14 | bitri 173 |
. . . . 5
⊢ (∀y ∈ B ∀z(z = 𝐶 → φ) ↔ ∀z(∃y ∈ B z = 𝐶 → φ)) |
16 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎzψ |
17 | | ralrnmpt2.2 |
. . . . . . . 8
⊢ (z = 𝐶 → (φ ↔ ψ)) |
18 | 16, 17 | ceqsalg 2576 |
. . . . . . 7
⊢ (𝐶 ∈ 𝑉 → (∀z(z = 𝐶 → φ) ↔ ψ)) |
19 | 18 | ralimi 2378 |
. . . . . 6
⊢ (∀y ∈ B 𝐶 ∈ 𝑉 → ∀y ∈ B (∀z(z = 𝐶 → φ) ↔ ψ)) |
20 | | ralbi 2439 |
. . . . . 6
⊢ (∀y ∈ B (∀z(z = 𝐶 → φ) ↔ ψ) → (∀y ∈ B ∀z(z = 𝐶 → φ) ↔ ∀y ∈ B ψ)) |
21 | 19, 20 | syl 14 |
. . . . 5
⊢ (∀y ∈ B 𝐶 ∈ 𝑉 → (∀y ∈ B ∀z(z = 𝐶 → φ) ↔ ∀y ∈ B ψ)) |
22 | 15, 21 | syl5bbr 183 |
. . . 4
⊢ (∀y ∈ B 𝐶 ∈ 𝑉 → (∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀y ∈ B ψ)) |
23 | 22 | ralimi 2378 |
. . 3
⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → ∀x ∈ A (∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀y ∈ B ψ)) |
24 | | ralbi 2439 |
. . 3
⊢ (∀x ∈ A (∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀y ∈ B ψ) → (∀x ∈ A ∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀x ∈ A ∀y ∈ B ψ)) |
25 | 23, 24 | syl 14 |
. 2
⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → (∀x ∈ A ∀z(∃y ∈ B z = 𝐶 → φ) ↔ ∀x ∈ A ∀y ∈ B ψ)) |
26 | 11, 25 | syl5bb 181 |
1
⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → (∀z ∈ ran 𝐹φ
↔ ∀x ∈ A ∀y ∈ B ψ)) |