Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. . 3
⊢ 𝑦 ∈ V |
2 | 1 | elint2 4417 |
. 2
⊢ (𝑦 ∈ ∩ {𝑥
∣ ∃𝑎 ∈
𝐴 𝑥 = (𝑎 “ 𝐵)} ↔ ∀𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}𝑦 ∈ 𝑧) |
3 | | elequ2 1991 |
. . . 4
⊢ (𝑧 = 𝑥 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑥)) |
4 | 3 | ralab2 3338 |
. . 3
⊢
(∀𝑧 ∈
{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}𝑦 ∈ 𝑧 ↔ ∀𝑥(∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵) → 𝑦 ∈ 𝑥)) |
5 | | df-rex 2902 |
. . . . . . 7
⊢
(∃𝑎 ∈
𝐴 𝑥 = (𝑎 “ 𝐵) ↔ ∃𝑎(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵))) |
6 | 5 | imbi1i 338 |
. . . . . 6
⊢
((∃𝑎 ∈
𝐴 𝑥 = (𝑎 “ 𝐵) → 𝑦 ∈ 𝑥) ↔ (∃𝑎(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥)) |
7 | | 19.23v 1889 |
. . . . . 6
⊢
(∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥) ↔ (∃𝑎(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥)) |
8 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑥 = (𝑎 “ 𝐵)) |
9 | 8 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝑎 “ 𝐵))) |
10 | 9 | pm5.74i 259 |
. . . . . . . 8
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ (𝑎 “ 𝐵))) |
11 | 1 | elima 5390 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑎 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 𝑏𝑎𝑦) |
12 | | df-br 4584 |
. . . . . . . . . . 11
⊢ (𝑏𝑎𝑦 ↔ 〈𝑏, 𝑦〉 ∈ 𝑎) |
13 | 12 | rexbii 3023 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
𝐵 𝑏𝑎𝑦 ↔ ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |
14 | 11, 13 | bitri 263 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑎 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |
15 | 14 | imbi2i 325 |
. . . . . . . 8
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ (𝑎 “ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
16 | 10, 15 | bitri 263 |
. . . . . . 7
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
17 | 16 | albii 1737 |
. . . . . 6
⊢
(∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥) ↔ ∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
18 | 6, 7, 17 | 3bitr2i 287 |
. . . . 5
⊢
((∃𝑎 ∈
𝐴 𝑥 = (𝑎 “ 𝐵) → 𝑦 ∈ 𝑥) ↔ ∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
19 | 18 | albii 1737 |
. . . 4
⊢
(∀𝑥(∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵) → 𝑦 ∈ 𝑥) ↔ ∀𝑥∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
20 | | 19.23v 1889 |
. . . . . . 7
⊢
(∀𝑥((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ (∃𝑥(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
21 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
22 | | imaexg 6995 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ V → (𝑎 “ 𝐵) ∈ V) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑎 “ 𝐵) ∈ V |
24 | 23 | isseti 3182 |
. . . . . . . . 9
⊢
∃𝑥 𝑥 = (𝑎 “ 𝐵) |
25 | | 19.42v 1905 |
. . . . . . . . 9
⊢
(∃𝑥(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) ↔ (𝑎 ∈ 𝐴 ∧ ∃𝑥 𝑥 = (𝑎 “ 𝐵))) |
26 | 24, 25 | mpbiran2 956 |
. . . . . . . 8
⊢
(∃𝑥(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) ↔ 𝑎 ∈ 𝐴) |
27 | 26 | imbi1i 338 |
. . . . . . 7
⊢
((∃𝑥(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ (𝑎 ∈ 𝐴 → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
28 | 20, 27 | bitri 263 |
. . . . . 6
⊢
(∀𝑥((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ (𝑎 ∈ 𝐴 → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
29 | 28 | albii 1737 |
. . . . 5
⊢
(∀𝑎∀𝑥((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ ∀𝑎(𝑎 ∈ 𝐴 → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
30 | | alcom 2024 |
. . . . 5
⊢
(∀𝑥∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ ∀𝑎∀𝑥((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
31 | | df-ral 2901 |
. . . . 5
⊢
(∀𝑎 ∈
𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎 ↔ ∀𝑎(𝑎 ∈ 𝐴 → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
32 | 29, 30, 31 | 3bitr4i 291 |
. . . 4
⊢
(∀𝑥∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |
33 | 19, 32 | bitri 263 |
. . 3
⊢
(∀𝑥(∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵) → 𝑦 ∈ 𝑥) ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |
34 | 4, 33 | bitri 263 |
. 2
⊢
(∀𝑧 ∈
{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}𝑦 ∈ 𝑧 ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |
35 | 2, 34 | bitri 263 |
1
⊢ (𝑦 ∈ ∩ {𝑥
∣ ∃𝑎 ∈
𝐴 𝑥 = (𝑎 “ 𝐵)} ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |