Step | Hyp | Ref
| Expression |
1 | | nfra1 3145 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 |
2 | | nfv 1916 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑡 ∈ 𝑧 |
3 | | eleq2 2839 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝑡 ∈ 𝑧 ↔ 𝑡 ∈ 𝐵)) |
4 | | vex 3411 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
5 | 4 | a1i 11 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝑡 ∈ 𝐵 → 𝑧 ∈ V) |
6 | | rspa 3133 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 𝑡 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑡 ∈ 𝐵) |
7 | 1, 2, 3, 5, 6 | elabreximd 30362 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝐴 𝑡 ∈ 𝐵 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) → 𝑡 ∈ 𝑧) |
8 | 7 | ex 417 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝑡 ∈ 𝐵 → (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) |
9 | 8 | alrimiv 1929 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝑡 ∈ 𝐵 → ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) |
10 | 9 | adantl 486 |
. . . 4
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵) → ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) |
11 | | nfra1 3145 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 |
12 | 2 | nfci 2900 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑧 |
13 | | nfre1 3228 |
. . . . . . . . . 10
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 = 𝐵 |
14 | 13 | nfab 2923 |
. . . . . . . . 9
⊢
Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} |
15 | 12, 14 | nfel 2931 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} |
16 | 15, 2 | nfim 1898 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧) |
17 | 16 | nfal 2332 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧) |
18 | 11, 17 | nfan 1901 |
. . . . 5
⊢
Ⅎ𝑥(∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) |
19 | | rspa 3133 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
20 | 19 | elexd 3429 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ V) |
21 | 20 | adantlr 715 |
. . . . . . 7
⊢
(((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ V) |
22 | | simplr 769 |
. . . . . . 7
⊢
(((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝑥 ∈ 𝐴) → ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) |
23 | | rspe 3226 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 = 𝐵) |
24 | | tbtru 1547 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝐴 𝑦 = 𝐵 ↔ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤)) |
25 | 23, 24 | sylib 221 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤)) |
26 | 25 | ex 417 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤))) |
27 | 26 | alrimiv 1929 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤))) |
28 | 27 | adantl 486 |
. . . . . . . 8
⊢
(((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤))) |
29 | | elabgt 3580 |
. . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ ∀𝑦(𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤))) → (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ⊤)) |
30 | | tbtru 1547 |
. . . . . . . . 9
⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ⊤)) |
31 | 29, 30 | sylibr 237 |
. . . . . . . 8
⊢ ((𝐵 ∈ V ∧ ∀𝑦(𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤))) → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
32 | 21, 28, 31 | syl2anc 588 |
. . . . . . 7
⊢
(((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
33 | | eleq1 2838 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐵 → (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})) |
34 | 33, 3 | imbi12d 349 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐵 → ((𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧) ↔ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝐵))) |
35 | 34 | spcgv 3511 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧) → (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝐵))) |
36 | 35 | imp 411 |
. . . . . . . 8
⊢ ((𝐵 ∈ V ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) → (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝐵)) |
37 | 36 | imp 411 |
. . . . . . 7
⊢ (((𝐵 ∈ V ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) → 𝑡 ∈ 𝐵) |
38 | 21, 22, 32, 37 | syl21anc 837 |
. . . . . 6
⊢
(((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) ∧ 𝑥 ∈ 𝐴) → 𝑡 ∈ 𝐵) |
39 | 38 | ex 417 |
. . . . 5
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) → (𝑥 ∈ 𝐴 → 𝑡 ∈ 𝐵)) |
40 | 18, 39 | ralrimi 3142 |
. . . 4
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 ∧ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)) → ∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵) |
41 | 10, 40 | impbida 801 |
. . 3
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧))) |
42 | 41 | abbidv 2823 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → {𝑡 ∣ ∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵} = {𝑡 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)}) |
43 | | df-iin 4879 |
. . 3
⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑡 ∣ ∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵} |
44 | 43 | a1i 11 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → ∩
𝑥 ∈ 𝐴 𝐵 = {𝑡 ∣ ∀𝑥 ∈ 𝐴 𝑡 ∈ 𝐵}) |
45 | | df-int 4832 |
. . 3
⊢ ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = 𝐵} = {𝑡 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)} |
46 | 45 | a1i 11 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑡 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑡 ∈ 𝑧)}) |
47 | 42, 44, 46 | 3eqtr4d 2804 |
1
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |