Step | Hyp | Ref
| Expression |
1 | | eluni 4439 |
. . 3
⊢ (𝑥 ∈ ∪ (𝑋
↾t 𝐴)
↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝑋 ↾t 𝐴))) |
2 | | elrest 16088 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑦 ∈ (𝑋 ↾t 𝐴) ↔ ∃𝑧 ∈ 𝑋 𝑦 = (𝑧 ∩ 𝐴))) |
3 | 2 | anbi2d 740 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝑋 ↾t 𝐴)) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑋 𝑦 = (𝑧 ∩ 𝐴)))) |
4 | 3 | exbidv 1850 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝑋 ↾t 𝐴)) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑋 𝑦 = (𝑧 ∩ 𝐴)))) |
5 | | eluni 4439 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑋
↔ ∃𝑧(𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋)) |
6 | 5 | bicomi 214 |
. . . . . . 7
⊢
(∃𝑧(𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) ↔ 𝑥 ∈ ∪ 𝑋) |
7 | 6 | anbi1i 731 |
. . . . . 6
⊢
((∃𝑧(𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ ∪ 𝑋 ∧ 𝑥 ∈ 𝐴)) |
8 | 7 | a1i 11 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ((∃𝑧(𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ ∪ 𝑋 ∧ 𝑥 ∈ 𝐴))) |
9 | | df-rex 2918 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
𝑋 𝑦 = (𝑧 ∩ 𝐴) ↔ ∃𝑧(𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴))) |
10 | 9 | anbi2i 730 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑋 𝑦 = (𝑧 ∩ 𝐴)) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑧(𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴)))) |
11 | | 19.42v 1918 |
. . . . . . . . 9
⊢
(∃𝑧(𝑥 ∈ 𝑦 ∧ (𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴))) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑧(𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴)))) |
12 | 11 | bicomi 214 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑦 ∧ ∃𝑧(𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴))) ↔ ∃𝑧(𝑥 ∈ 𝑦 ∧ (𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴)))) |
13 | 10, 12 | bitri 264 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑋 𝑦 = (𝑧 ∩ 𝐴)) ↔ ∃𝑧(𝑥 ∈ 𝑦 ∧ (𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴)))) |
14 | 13 | exbii 1774 |
. . . . . 6
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑋 𝑦 = (𝑧 ∩ 𝐴)) ↔ ∃𝑦∃𝑧(𝑥 ∈ 𝑦 ∧ (𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴)))) |
15 | | excom 2042 |
. . . . . 6
⊢
(∃𝑦∃𝑧(𝑥 ∈ 𝑦 ∧ (𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴))) ↔ ∃𝑧∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴)))) |
16 | | an12 838 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑦 ∧ (𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴))) ↔ (𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 = (𝑧 ∩ 𝐴)))) |
17 | 16 | exbii 1774 |
. . . . . . . . 9
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴))) ↔ ∃𝑦(𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 = (𝑧 ∩ 𝐴)))) |
18 | | 19.42v 1918 |
. . . . . . . . 9
⊢
(∃𝑦(𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 = (𝑧 ∩ 𝐴))) ↔ (𝑧 ∈ 𝑋 ∧ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 = (𝑧 ∩ 𝐴)))) |
19 | | eqimss 3657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑧 ∩ 𝐴) → 𝑦 ⊆ (𝑧 ∩ 𝐴)) |
20 | 19 | sseld 3602 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑧 ∩ 𝐴) → (𝑥 ∈ 𝑦 → 𝑥 ∈ (𝑧 ∩ 𝐴))) |
21 | 20 | imdistanri 727 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 = (𝑧 ∩ 𝐴)) → (𝑥 ∈ (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑧 ∩ 𝐴))) |
22 | | eqimss2 3658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑧 ∩ 𝐴) → (𝑧 ∩ 𝐴) ⊆ 𝑦) |
23 | 22 | sseld 3602 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑧 ∩ 𝐴) → (𝑥 ∈ (𝑧 ∩ 𝐴) → 𝑥 ∈ 𝑦)) |
24 | 23 | imdistanri 727 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑧 ∩ 𝐴)) → (𝑥 ∈ 𝑦 ∧ 𝑦 = (𝑧 ∩ 𝐴))) |
25 | 21, 24 | impbii 199 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 = (𝑧 ∩ 𝐴)) ↔ (𝑥 ∈ (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑧 ∩ 𝐴))) |
26 | 25 | exbii 1774 |
. . . . . . . . . . . 12
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 = (𝑧 ∩ 𝐴)) ↔ ∃𝑦(𝑥 ∈ (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑧 ∩ 𝐴))) |
27 | | 19.42v 1918 |
. . . . . . . . . . . 12
⊢
(∃𝑦(𝑥 ∈ (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑧 ∩ 𝐴)) ↔ (𝑥 ∈ (𝑧 ∩ 𝐴) ∧ ∃𝑦 𝑦 = (𝑧 ∩ 𝐴))) |
28 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
29 | 28 | inex1 4799 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∩ 𝐴) ∈ V |
30 | 29 | isseti 3209 |
. . . . . . . . . . . . . . 15
⊢
∃𝑦 𝑦 = (𝑧 ∩ 𝐴) |
31 | 30 | biantru 526 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑧 ∩ 𝐴) ↔ (𝑥 ∈ (𝑧 ∩ 𝐴) ∧ ∃𝑦 𝑦 = (𝑧 ∩ 𝐴))) |
32 | 31 | bicomi 214 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝑧 ∩ 𝐴) ∧ ∃𝑦 𝑦 = (𝑧 ∩ 𝐴)) ↔ 𝑥 ∈ (𝑧 ∩ 𝐴)) |
33 | | elin 3796 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑧 ∩ 𝐴) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐴)) |
34 | 32, 33 | bitri 264 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑧 ∩ 𝐴) ∧ ∃𝑦 𝑦 = (𝑧 ∩ 𝐴)) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐴)) |
35 | 26, 27, 34 | 3bitri 286 |
. . . . . . . . . . 11
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 = (𝑧 ∩ 𝐴)) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐴)) |
36 | 35 | anbi2i 730 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ∧ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 = (𝑧 ∩ 𝐴))) ↔ (𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐴))) |
37 | | biid 251 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐴)) |
38 | 37 | bianass 842 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝐴)) ↔ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑧) ∧ 𝑥 ∈ 𝐴)) |
39 | | ancom 466 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑧) ↔ (𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋)) |
40 | 39 | anbi1i 731 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑧) ∧ 𝑥 ∈ 𝐴) ↔ ((𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴)) |
41 | 36, 38, 40 | 3bitri 286 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ∧ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 = (𝑧 ∩ 𝐴))) ↔ ((𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴)) |
42 | 17, 18, 41 | 3bitri 286 |
. . . . . . . 8
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴))) ↔ ((𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴)) |
43 | 42 | exbii 1774 |
. . . . . . 7
⊢
(∃𝑧∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴))) ↔ ∃𝑧((𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴)) |
44 | | 19.41v 1914 |
. . . . . . 7
⊢
(∃𝑧((𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴) ↔ (∃𝑧(𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴)) |
45 | 43, 44 | bitri 264 |
. . . . . 6
⊢
(∃𝑧∃𝑦(𝑥 ∈ 𝑦 ∧ (𝑧 ∈ 𝑋 ∧ 𝑦 = (𝑧 ∩ 𝐴))) ↔ (∃𝑧(𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴)) |
46 | 14, 15, 45 | 3bitri 286 |
. . . . 5
⊢
(∃𝑦(𝑥 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑋 𝑦 = (𝑧 ∩ 𝐴)) ↔ (∃𝑧(𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝐴)) |
47 | | elin 3796 |
. . . . 5
⊢ (𝑥 ∈ (∪ 𝑋
∩ 𝐴) ↔ (𝑥 ∈ ∪ 𝑋
∧ 𝑥 ∈ 𝐴)) |
48 | 8, 46, 47 | 3bitr4g 303 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∃𝑦(𝑥 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑋 𝑦 = (𝑧 ∩ 𝐴)) ↔ 𝑥 ∈ (∪ 𝑋 ∩ 𝐴))) |
49 | 4, 48 | bitrd 268 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝑋 ↾t 𝐴)) ↔ 𝑥 ∈ (∪ 𝑋 ∩ 𝐴))) |
50 | 1, 49 | syl5bb 272 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑥 ∈ ∪ (𝑋 ↾t 𝐴) ↔ 𝑥 ∈ (∪ 𝑋 ∩ 𝐴))) |
51 | 50 | eqrdv 2620 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋
∩ 𝐴)) |