Step | Hyp | Ref
| Expression |
1 | | vex 3417 |
. . 3
⊢ 𝑦 ∈ V |
2 | 1 | elint2 4871 |
. 2
⊢ (𝑦 ∈ ∩ {𝑥
∣ ∃𝑎 ∈
𝐴 𝑥 = (𝑎 “ 𝐵)} ↔ ∀𝑧 ∈ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}𝑦 ∈ 𝑧) |
3 | | elequ2 2125 |
. . . 4
⊢ (𝑧 = 𝑥 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑥)) |
4 | 3 | ralab2 3615 |
. . 3
⊢
(∀𝑧 ∈
{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}𝑦 ∈ 𝑧 ↔ ∀𝑥(∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵) → 𝑦 ∈ 𝑥)) |
5 | | df-rex 3067 |
. . . . . . 7
⊢
(∃𝑎 ∈
𝐴 𝑥 = (𝑎 “ 𝐵) ↔ ∃𝑎(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵))) |
6 | 5 | imbi1i 353 |
. . . . . 6
⊢
((∃𝑎 ∈
𝐴 𝑥 = (𝑎 “ 𝐵) → 𝑦 ∈ 𝑥) ↔ (∃𝑎(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥)) |
7 | | 19.23v 1950 |
. . . . . 6
⊢
(∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥) ↔ (∃𝑎(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥)) |
8 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑥 = (𝑎 “ 𝐵)) |
9 | 8 | eleq2d 2823 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝑎 “ 𝐵))) |
10 | 9 | pm5.74i 274 |
. . . . . . . 8
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ (𝑎 “ 𝐵))) |
11 | 1 | elima 5939 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑎 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 𝑏𝑎𝑦) |
12 | | df-br 5059 |
. . . . . . . . . . 11
⊢ (𝑏𝑎𝑦 ↔ 〈𝑏, 𝑦〉 ∈ 𝑎) |
13 | 12 | rexbii 3175 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
𝐵 𝑏𝑎𝑦 ↔ ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |
14 | 11, 13 | bitri 278 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑎 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |
15 | 14 | imbi2i 339 |
. . . . . . . 8
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ (𝑎 “ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
16 | 10, 15 | bitri 278 |
. . . . . . 7
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
17 | 16 | albii 1827 |
. . . . . 6
⊢
(∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → 𝑦 ∈ 𝑥) ↔ ∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
18 | 6, 7, 17 | 3bitr2i 302 |
. . . . 5
⊢
((∃𝑎 ∈
𝐴 𝑥 = (𝑎 “ 𝐵) → 𝑦 ∈ 𝑥) ↔ ∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
19 | 18 | albii 1827 |
. . . 4
⊢
(∀𝑥(∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵) → 𝑦 ∈ 𝑥) ↔ ∀𝑥∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
20 | | 19.23v 1950 |
. . . . . . 7
⊢
(∀𝑥((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ (∃𝑥(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
21 | | vex 3417 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
22 | 21 | imaex 7699 |
. . . . . . . . . 10
⊢ (𝑎 “ 𝐵) ∈ V |
23 | 22 | isseti 3428 |
. . . . . . . . 9
⊢
∃𝑥 𝑥 = (𝑎 “ 𝐵) |
24 | | 19.42v 1962 |
. . . . . . . . 9
⊢
(∃𝑥(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) ↔ (𝑎 ∈ 𝐴 ∧ ∃𝑥 𝑥 = (𝑎 “ 𝐵))) |
25 | 23, 24 | mpbiran2 710 |
. . . . . . . 8
⊢
(∃𝑥(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) ↔ 𝑎 ∈ 𝐴) |
26 | 25 | imbi1i 353 |
. . . . . . 7
⊢
((∃𝑥(𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ (𝑎 ∈ 𝐴 → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
27 | 20, 26 | bitri 278 |
. . . . . 6
⊢
(∀𝑥((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ (𝑎 ∈ 𝐴 → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
28 | 27 | albii 1827 |
. . . . 5
⊢
(∀𝑎∀𝑥((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ ∀𝑎(𝑎 ∈ 𝐴 → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
29 | | alcom 2160 |
. . . . 5
⊢
(∀𝑥∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ ∀𝑎∀𝑥((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
30 | | df-ral 3066 |
. . . . 5
⊢
(∀𝑎 ∈
𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎 ↔ ∀𝑎(𝑎 ∈ 𝐴 → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎)) |
31 | 28, 29, 30 | 3bitr4i 306 |
. . . 4
⊢
(∀𝑥∀𝑎((𝑎 ∈ 𝐴 ∧ 𝑥 = (𝑎 “ 𝐵)) → ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |
32 | 19, 31 | bitri 278 |
. . 3
⊢
(∀𝑥(∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵) → 𝑦 ∈ 𝑥) ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |
33 | 4, 32 | bitri 278 |
. 2
⊢
(∀𝑧 ∈
{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}𝑦 ∈ 𝑧 ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |
34 | 2, 33 | bitri 278 |
1
⊢ (𝑦 ∈ ∩ {𝑥
∣ ∃𝑎 ∈
𝐴 𝑥 = (𝑎 “ 𝐵)} ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 〈𝑏, 𝑦〉 ∈ 𝑎) |