Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . . 6
⊢
Ⅎ𝑑(𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) |
2 | | nfv 1918 |
. . . . . . 7
⊢
Ⅎ𝑑 𝑐 ⊆ ∪ (𝐽
↾t 𝐴) |
3 | | nfre1 3283 |
. . . . . . 7
⊢
Ⅎ𝑑∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) |
4 | 2, 3 | nfan 1903 |
. . . . . 6
⊢
Ⅎ𝑑(𝑐 ⊆ ∪ (𝐽
↾t 𝐴)
∧ ∃𝑑 ∈
(𝐽 ↾t
𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) |
5 | 1, 4 | nfan 1903 |
. . . . 5
⊢
Ⅎ𝑑((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) |
6 | | simpl 484 |
. . . . . . 7
⊢ ((𝑐 ⊆ ∪ (𝐽
↾t 𝐴)
∧ ∃𝑑 ∈
(𝐽 ↾t
𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) |
7 | 6 | anim2i 618 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴))) |
8 | | simp-5r 785 |
. . . . . . . . . . 11
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) |
9 | | simp1 1137 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐽 ∈ Top) |
10 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 ⊆ 𝑋) |
11 | | neitr.1 |
. . . . . . . . . . . . . 14
⊢ 𝑋 = ∪
𝐽 |
12 | 11 | restuni 22658 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
13 | 9, 10, 12 | syl2anc 585 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
14 | 13 | ad5antr 733 |
. . . . . . . . . . 11
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
15 | 8, 14 | sseqtrrd 4023 |
. . . . . . . . . 10
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ 𝐴) |
16 | 10 | ad5antr 733 |
. . . . . . . . . 10
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐴 ⊆ 𝑋) |
17 | 15, 16 | sstrd 3992 |
. . . . . . . . 9
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 ⊆ 𝑋) |
18 | 9 | ad5antr 733 |
. . . . . . . . . . 11
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐽 ∈ Top) |
19 | | simplr 768 |
. . . . . . . . . . 11
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ∈ 𝐽) |
20 | 11 | eltopss 22401 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑒 ∈ 𝐽) → 𝑒 ⊆ 𝑋) |
21 | 18, 19, 20 | syl2anc 585 |
. . . . . . . . . 10
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ⊆ 𝑋) |
22 | 21 | ssdifssd 4142 |
. . . . . . . . 9
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑒 ∖ 𝐴) ⊆ 𝑋) |
23 | 17, 22 | unssd 4186 |
. . . . . . . 8
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋) |
24 | | simpr1l 1231 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ∧ 𝑒 ∈ 𝐽 ∧ 𝑑 = (𝑒 ∩ 𝐴))) → 𝐵 ⊆ 𝑑) |
25 | 24 | 3anassrs 1361 |
. . . . . . . . . . 11
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ 𝑑) |
26 | | simpr 486 |
. . . . . . . . . . 11
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑑 = (𝑒 ∩ 𝐴)) |
27 | 25, 26 | sseqtrd 4022 |
. . . . . . . . . 10
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ (𝑒 ∩ 𝐴)) |
28 | | inss1 4228 |
. . . . . . . . . 10
⊢ (𝑒 ∩ 𝐴) ⊆ 𝑒 |
29 | 27, 28 | sstrdi 3994 |
. . . . . . . . 9
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝐵 ⊆ 𝑒) |
30 | | inundif 4478 |
. . . . . . . . . 10
⊢ ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) = 𝑒 |
31 | | simpr1r 1232 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ∧ 𝑒 ∈ 𝐽 ∧ 𝑑 = (𝑒 ∩ 𝐴))) → 𝑑 ⊆ 𝑐) |
32 | 31 | 3anassrs 1361 |
. . . . . . . . . . . 12
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑑 ⊆ 𝑐) |
33 | 26, 32 | eqsstrrd 4021 |
. . . . . . . . . . 11
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → (𝑒 ∩ 𝐴) ⊆ 𝑐) |
34 | | unss1 4179 |
. . . . . . . . . . 11
⊢ ((𝑒 ∩ 𝐴) ⊆ 𝑐 → ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))) |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ((𝑒 ∩ 𝐴) ∪ (𝑒 ∖ 𝐴)) ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))) |
36 | 30, 35 | eqsstrrid 4031 |
. . . . . . . . 9
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))) |
37 | | sseq2 4008 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑒 → (𝐵 ⊆ 𝑏 ↔ 𝐵 ⊆ 𝑒)) |
38 | | sseq1 4007 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑒 → (𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)) ↔ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) |
39 | 37, 38 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑒 → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))) ↔ (𝐵 ⊆ 𝑒 ∧ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))) |
40 | 39 | rspcev 3613 |
. . . . . . . . 9
⊢ ((𝑒 ∈ 𝐽 ∧ (𝐵 ⊆ 𝑒 ∧ 𝑒 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) → ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) |
41 | 19, 29, 36, 40 | syl12anc 836 |
. . . . . . . 8
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) |
42 | | indir 4275 |
. . . . . . . . . . 11
⊢ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴) = ((𝑐 ∩ 𝐴) ∪ ((𝑒 ∖ 𝐴) ∩ 𝐴)) |
43 | | disjdifr 4472 |
. . . . . . . . . . . 12
⊢ ((𝑒 ∖ 𝐴) ∩ 𝐴) = ∅ |
44 | 43 | uneq2i 4160 |
. . . . . . . . . . 11
⊢ ((𝑐 ∩ 𝐴) ∪ ((𝑒 ∖ 𝐴) ∩ 𝐴)) = ((𝑐 ∩ 𝐴) ∪ ∅) |
45 | | un0 4390 |
. . . . . . . . . . 11
⊢ ((𝑐 ∩ 𝐴) ∪ ∅) = (𝑐 ∩ 𝐴) |
46 | 42, 44, 45 | 3eqtri 2765 |
. . . . . . . . . 10
⊢ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴) = (𝑐 ∩ 𝐴) |
47 | | df-ss 3965 |
. . . . . . . . . . 11
⊢ (𝑐 ⊆ 𝐴 ↔ (𝑐 ∩ 𝐴) = 𝑐) |
48 | 47 | biimpi 215 |
. . . . . . . . . 10
⊢ (𝑐 ⊆ 𝐴 → (𝑐 ∩ 𝐴) = 𝑐) |
49 | 46, 48 | eqtr2id 2786 |
. . . . . . . . 9
⊢ (𝑐 ⊆ 𝐴 → 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴)) |
50 | 15, 49 | syl 17 |
. . . . . . . 8
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴)) |
51 | | vex 3479 |
. . . . . . . . . 10
⊢ 𝑐 ∈ V |
52 | | vex 3479 |
. . . . . . . . . . 11
⊢ 𝑒 ∈ V |
53 | 52 | difexi 5328 |
. . . . . . . . . 10
⊢ (𝑒 ∖ 𝐴) ∈ V |
54 | 51, 53 | unex 7730 |
. . . . . . . . 9
⊢ (𝑐 ∪ (𝑒 ∖ 𝐴)) ∈ V |
55 | | sseq1 4007 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑎 ⊆ 𝑋 ↔ (𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋)) |
56 | | sseq2 4008 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑏 ⊆ 𝑎 ↔ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) |
57 | 56 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) ↔ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))) |
58 | 57 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) ↔ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴))))) |
59 | 55, 58 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → ((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ↔ ((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))))) |
60 | | ineq1 4205 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑎 ∩ 𝐴) = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴)) |
61 | 60 | eqeq2d 2744 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (𝑐 = (𝑎 ∩ 𝐴) ↔ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴))) |
62 | 59, 61 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑎 = (𝑐 ∪ (𝑒 ∖ 𝐴)) → (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ (((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴)))) |
63 | 54, 62 | spcev 3597 |
. . . . . . . 8
⊢ ((((𝑐 ∪ (𝑒 ∖ 𝐴)) ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ (𝑐 ∪ (𝑒 ∖ 𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒 ∖ 𝐴)) ∩ 𝐴)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) |
64 | 23, 41, 50, 63 | syl21anc 837 |
. . . . . . 7
⊢
(((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ∧ 𝑒 ∈ 𝐽) ∧ 𝑑 = (𝑒 ∩ 𝐴)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) |
65 | 9 | ad3antrrr 729 |
. . . . . . . 8
⊢
(((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝐽 ∈ Top) |
66 | 9 | uniexd 7729 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ∪ 𝐽 ∈ V) |
67 | 11, 66 | eqeltrid 2838 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝑋 ∈ V) |
68 | 67, 10 | ssexd 5324 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐴 ∈ V) |
69 | 68 | ad3antrrr 729 |
. . . . . . . 8
⊢
(((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝐴 ∈ V) |
70 | | simplr 768 |
. . . . . . . 8
⊢
(((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → 𝑑 ∈ (𝐽 ↾t 𝐴)) |
71 | | elrest 17370 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝑑 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴))) |
72 | 71 | biimpa 478 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ V) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) → ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴)) |
73 | 65, 69, 70, 72 | syl21anc 837 |
. . . . . . 7
⊢
(((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑒 ∈ 𝐽 𝑑 = (𝑒 ∩ 𝐴)) |
74 | 64, 73 | r19.29a 3163 |
. . . . . 6
⊢
(((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) |
75 | 7, 74 | sylanl1 679 |
. . . . 5
⊢
(((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) ∧ 𝑑 ∈ (𝐽 ↾t 𝐴)) ∧ (𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) |
76 | | simprr 772 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) |
77 | 5, 75, 76 | r19.29af 3266 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) → ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) |
78 | | inss2 4229 |
. . . . . . . . . 10
⊢ (𝑎 ∩ 𝐴) ⊆ 𝐴 |
79 | | sseq1 4007 |
. . . . . . . . . 10
⊢ (𝑐 = (𝑎 ∩ 𝐴) → (𝑐 ⊆ 𝐴 ↔ (𝑎 ∩ 𝐴) ⊆ 𝐴)) |
80 | 78, 79 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑐 = (𝑎 ∩ 𝐴) → 𝑐 ⊆ 𝐴) |
81 | 80 | adantl 483 |
. . . . . . . 8
⊢ (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → 𝑐 ⊆ 𝐴) |
82 | 81 | exlimiv 1934 |
. . . . . . 7
⊢
(∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → 𝑐 ⊆ 𝐴) |
83 | 82 | adantl 483 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝑐 ⊆ 𝐴) |
84 | 13 | adantr 482 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
85 | 83, 84 | sseqtrd 4022 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → 𝑐 ⊆ ∪ (𝐽 ↾t 𝐴)) |
86 | 9 | ad4antr 731 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐽 ∈ Top) |
87 | 68 | ad4antr 731 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐴 ∈ V) |
88 | | simplr 768 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑏 ∈ 𝐽) |
89 | | elrestr 17371 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ 𝑏 ∈ 𝐽) → (𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
90 | 86, 87, 88, 89 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
91 | | simprl 770 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ 𝑏) |
92 | | simp3 1139 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐴) |
93 | 92 | ad4antr 731 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ 𝐴) |
94 | 91, 93 | ssind 4232 |
. . . . . . . . . . . . . 14
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝐵 ⊆ (𝑏 ∩ 𝐴)) |
95 | | simprr 772 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑏 ⊆ 𝑎) |
96 | 95 | ssrind 4235 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ⊆ (𝑎 ∩ 𝐴)) |
97 | | simp-4r 783 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → 𝑐 = (𝑎 ∩ 𝐴)) |
98 | 96, 97 | sseqtrrd 4023 |
. . . . . . . . . . . . . 14
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → (𝑏 ∩ 𝐴) ⊆ 𝑐) |
99 | 90, 94, 98 | jca32 517 |
. . . . . . . . . . . . 13
⊢
((((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) ∧ (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) → ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))) |
100 | 99 | ex 414 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈ Top
∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ 𝐽) → ((𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) → ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))) |
101 | 100 | reximdva 3169 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ 𝑎 ⊆ 𝑋) → (∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))) |
102 | 101 | impr 456 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ∧ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎))) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))) |
103 | 102 | an32s 651 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎))) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))) |
104 | 103 | expl 459 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))) |
105 | 104 | exlimdv 1937 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)))) |
106 | 105 | imp 408 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → ∃𝑏 ∈ 𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))) |
107 | | sseq2 4008 |
. . . . . . . . 9
⊢ (𝑑 = (𝑏 ∩ 𝐴) → (𝐵 ⊆ 𝑑 ↔ 𝐵 ⊆ (𝑏 ∩ 𝐴))) |
108 | | sseq1 4007 |
. . . . . . . . 9
⊢ (𝑑 = (𝑏 ∩ 𝐴) → (𝑑 ⊆ 𝑐 ↔ (𝑏 ∩ 𝐴) ⊆ 𝑐)) |
109 | 107, 108 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑑 = (𝑏 ∩ 𝐴) → ((𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐) ↔ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐))) |
110 | 109 | rspcev 3613 |
. . . . . . 7
⊢ (((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) |
111 | 110 | rexlimivw 3152 |
. . . . . 6
⊢
(∃𝑏 ∈
𝐽 ((𝑏 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ (𝐵 ⊆ (𝑏 ∩ 𝐴) ∧ (𝑏 ∩ 𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) |
112 | 106, 111 | syl 17 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) |
113 | 85, 112 | jca 513 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴))) → (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐))) |
114 | 77, 113 | impbida 800 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))) |
115 | | resttop 22656 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top) |
116 | 9, 68, 115 | syl2anc 585 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝐽 ↾t 𝐴) ∈ Top) |
117 | 92, 13 | sseqtrd 4022 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ ∪ (𝐽 ↾t 𝐴)) |
118 | | eqid 2733 |
. . . . 5
⊢ ∪ (𝐽
↾t 𝐴) =
∪ (𝐽 ↾t 𝐴) |
119 | 118 | isnei 22599 |
. . . 4
⊢ (((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐵 ⊆ ∪ (𝐽
↾t 𝐴))
→ (𝑐 ∈
((nei‘(𝐽
↾t 𝐴))‘𝐵) ↔ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)))) |
120 | 116, 117,
119 | syl2anc 585 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ((nei‘(𝐽 ↾t 𝐴))‘𝐵) ↔ (𝑐 ⊆ ∪ (𝐽 ↾t 𝐴) ∧ ∃𝑑 ∈ (𝐽 ↾t 𝐴)(𝐵 ⊆ 𝑑 ∧ 𝑑 ⊆ 𝑐)))) |
121 | | fvex 6902 |
. . . . . 6
⊢
((nei‘𝐽)‘𝐵) ∈ V |
122 | | restval 17369 |
. . . . . 6
⊢
((((nei‘𝐽)‘𝐵) ∈ V ∧ 𝐴 ∈ V) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴))) |
123 | 121, 68, 122 | sylancr 588 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴))) |
124 | 123 | eleq2d 2820 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ 𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)))) |
125 | 92, 10 | sstrd 3992 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝑋) |
126 | | eqid 2733 |
. . . . . . . . 9
⊢ (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) = (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) |
127 | 126 | elrnmpt 5954 |
. . . . . . . 8
⊢ (𝑐 ∈ V → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴))) |
128 | 127 | elv 3481 |
. . . . . . 7
⊢ (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴)) |
129 | | df-rex 3072 |
. . . . . . 7
⊢
(∃𝑎 ∈
((nei‘𝐽)‘𝐵)𝑐 = (𝑎 ∩ 𝐴) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴))) |
130 | 128, 129 | bitri 275 |
. . . . . 6
⊢ (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴))) |
131 | 11 | isnei 22599 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↔ (𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)))) |
132 | 131 | anbi1d 631 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → ((𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ ((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))) |
133 | 132 | exbidv 1925 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))) |
134 | 130, 133 | bitrid 283 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))) |
135 | 9, 125, 134 | syl2anc 585 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎 ∩ 𝐴)) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))) |
136 | 124, 135 | bitrd 279 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ ∃𝑎((𝑎 ⊆ 𝑋 ∧ ∃𝑏 ∈ 𝐽 (𝐵 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑎)) ∧ 𝑐 = (𝑎 ∩ 𝐴)))) |
137 | 114, 120,
136 | 3bitr4d 311 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → (𝑐 ∈ ((nei‘(𝐽 ↾t 𝐴))‘𝐵) ↔ 𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴))) |
138 | 137 | eqrdv 2731 |
1
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴)) |