Step | Hyp | Ref
| Expression |
1 | | df-ral 3069 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 𝑤 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵)) |
2 | | df-ral 3069 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶)) |
3 | | eleq2 2827 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵)) |
4 | 3 | biimprcd 249 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐵 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) |
5 | 4 | alrimiv 1930 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐵 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) |
6 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ 𝐵 = 𝐵 |
7 | | eqeq1 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝐵 → (𝑧 = 𝐵 ↔ 𝐵 = 𝐵)) |
8 | 7, 3 | imbi12d 345 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝐵 → ((𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (𝐵 = 𝐵 → 𝑤 ∈ 𝐵))) |
9 | 8 | spcgv 3532 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝐶 → (∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧) → (𝐵 = 𝐵 → 𝑤 ∈ 𝐵))) |
10 | 6, 9 | mpii 46 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝐶 → (∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧) → 𝑤 ∈ 𝐵)) |
11 | 5, 10 | impbid2 225 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝐶 → (𝑤 ∈ 𝐵 ↔ ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))) |
12 | 11 | imim2i 16 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → (𝑥 ∈ 𝐴 → (𝑤 ∈ 𝐵 ↔ ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))) |
13 | 12 | pm5.74d 272 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))) |
14 | 13 | alimi 1814 |
. . . . . . 7
⊢
(∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → ∀𝑥((𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))) |
15 | | albi 1821 |
. . . . . . 7
⊢
(∀𝑥((𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))) → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢
(∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))) |
17 | 2, 16 | sylbi 216 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))) |
18 | | df-ral 3069 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧))) |
19 | 18 | albii 1822 |
. . . . . . 7
⊢
(∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑧∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧))) |
20 | | alcom 2156 |
. . . . . . 7
⊢
(∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑧∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧))) |
21 | 19, 20 | bitr4i 277 |
. . . . . 6
⊢
(∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧))) |
22 | | r19.23v 3206 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) |
23 | | vex 3433 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
24 | | eqeq1 2742 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑧 = 𝐵)) |
25 | 24 | rexbidv 3224 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
26 | 23, 25 | elab 3608 |
. . . . . . . . 9
⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
27 | 26 | imbi1i 350 |
. . . . . . . 8
⊢ ((𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧) ↔ (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) |
28 | 22, 27 | bitr4i 277 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)) |
29 | 28 | albii 1822 |
. . . . . 6
⊢
(∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)) |
30 | | 19.21v 1942 |
. . . . . . 7
⊢
(∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))) |
31 | 30 | albii 1822 |
. . . . . 6
⊢
(∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))) |
32 | 21, 29, 31 | 3bitr3ri 302 |
. . . . 5
⊢
(∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)) |
33 | 17, 32 | bitrdi 287 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧))) |
34 | 1, 33 | bitrid 282 |
. . 3
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → (∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧))) |
35 | 34 | abbidv 2807 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → {𝑤 ∣ ∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)}) |
36 | | df-iin 4927 |
. 2
⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑤 ∣ ∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵} |
37 | | df-int 4880 |
. 2
⊢ ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)} |
38 | 35, 36, 37 | 3eqtr4g 2803 |
1
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |