Step | Hyp | Ref
| Expression |
1 | | uniss 4683 |
. . . . . . 7
⊢ (𝑒 ⊆ 𝐽 → ∪ 𝑒 ⊆ ∪ 𝐽) |
2 | 1 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ⊆ ∪ 𝐽) |
3 | | neiptop.o |
. . . . . . . 8
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} |
4 | | neiptop.0 |
. . . . . . . 8
⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) |
5 | | neiptop.1 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) |
6 | | neiptop.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) |
7 | | neiptop.3 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) |
8 | | neiptop.4 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) |
9 | | neiptop.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) |
10 | 3, 4, 5, 6, 7, 8, 9 | neiptopuni 21312 |
. . . . . . 7
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
11 | 10 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑋 = ∪ 𝐽) |
12 | 2, 11 | sseqtr4d 3867 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ⊆ 𝑋) |
13 | | simp-4l 801 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝜑) |
14 | 12 | ad3antrrr 721 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ⊆ 𝑋) |
15 | | simpllr 793 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ ∪ 𝑒) |
16 | 14, 15 | sseldd 3828 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ 𝑋) |
17 | 13, 16 | jca 507 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → (𝜑 ∧ 𝑝 ∈ 𝑋)) |
18 | | elssuni 4691 |
. . . . . . . . . 10
⊢ (𝑐 ∈ 𝑒 → 𝑐 ⊆ ∪ 𝑒) |
19 | 18 | ad2antlr 718 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ⊆ ∪ 𝑒) |
20 | 17, 19, 14 | 3jca 1162 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋)) |
21 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ⊆ 𝐽) |
22 | 21 | sselda 3827 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → 𝑐 ∈ 𝐽) |
23 | 3 | neipeltop 21311 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ 𝐽 ↔ (𝑐 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝))) |
24 | 23 | simprbi 492 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ 𝐽 → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝)) |
25 | 22, 24 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝)) |
26 | 25 | r19.21bi 3141 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝)) |
27 | 26 | adantllr 710 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝)) |
28 | | sseq1 3851 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑐 → (𝑎 ⊆ ∪ 𝑒 ↔ 𝑐 ⊆ ∪ 𝑒)) |
29 | 28 | 3anbi2d 1569 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋))) |
30 | | eleq1 2894 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝))) |
31 | 29, 30 | anbi12d 624 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)))) |
32 | 31 | imbi1d 333 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑐 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))) |
33 | 32 | imbi2d 332 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) ↔ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))))) |
34 | | ssidd 3849 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ⊆ 𝑋) |
35 | 9 | ralrimiva 3175 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝)) |
36 | 3 | neipeltop 21311 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ 𝐽 ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝))) |
37 | 34, 35, 36 | sylanbrc 578 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ 𝐽) |
38 | | pwexg 5080 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V) |
39 | | rabexg 5038 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 𝑋 ∈
V → {𝑎 ∈
𝒫 𝑋 ∣
∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V) |
40 | 37, 38, 39 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V) |
41 | 3, 40 | syl5eqel 2910 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ V) |
42 | 41 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝐽 ∈ V) |
43 | 42, 21 | ssexd 5032 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ∈ V) |
44 | | uniexg 7220 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ V → ∪ 𝑒
∈ V) |
45 | | sseq2 3852 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = ∪
𝑒 → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ ∪ 𝑒)) |
46 | | sseq1 3851 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = ∪
𝑒 → (𝑏 ⊆ 𝑋 ↔ ∪ 𝑒 ⊆ 𝑋)) |
47 | 45, 46 | 3anbi23d 1567 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = ∪
𝑒 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋))) |
48 | 47 | anbi1d 623 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ∪
𝑒 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)))) |
49 | | eleq1 2894 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ∪
𝑒 → (𝑏 ∈ (𝑁‘𝑝) ↔ ∪ 𝑒 ∈ (𝑁‘𝑝))) |
50 | 48, 49 | imbi12d 336 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∪
𝑒 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))) |
51 | 50, 5 | vtoclg 3482 |
. . . . . . . . . . 11
⊢ (∪ 𝑒
∈ V → ((((𝜑 ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) |
52 | 43, 44, 51 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) |
53 | 33, 52 | chvarv 2416 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) |
54 | 53 | ad3antrrr 721 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) |
55 | 20, 27, 54 | mp2and 690 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ∈ (𝑁‘𝑝)) |
56 | | simpr 479 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → 𝑝 ∈ ∪ 𝑒) |
57 | | eluni2 4664 |
. . . . . . . 8
⊢ (𝑝 ∈ ∪ 𝑒
↔ ∃𝑐 ∈
𝑒 𝑝 ∈ 𝑐) |
58 | 56, 57 | sylib 210 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∃𝑐 ∈ 𝑒 𝑝 ∈ 𝑐) |
59 | 55, 58 | r19.29a 3288 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∪ 𝑒
∈ (𝑁‘𝑝)) |
60 | 59 | ralrimiva 3175 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∀𝑝 ∈ ∪ 𝑒∪
𝑒 ∈ (𝑁‘𝑝)) |
61 | 3 | neipeltop 21311 |
. . . . 5
⊢ (∪ 𝑒
∈ 𝐽 ↔ (∪ 𝑒
⊆ 𝑋 ∧
∀𝑝 ∈ ∪ 𝑒∪ 𝑒 ∈ (𝑁‘𝑝))) |
62 | 12, 60, 61 | sylanbrc 578 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ∈ 𝐽) |
63 | 62 | ex 403 |
. . 3
⊢ (𝜑 → (𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽)) |
64 | 63 | alrimiv 2026 |
. 2
⊢ (𝜑 → ∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽)) |
65 | | inss1 4059 |
. . . . . 6
⊢ (𝑒 ∩ 𝑓) ⊆ 𝑒 |
66 | 3 | neipeltop 21311 |
. . . . . . . 8
⊢ (𝑒 ∈ 𝐽 ↔ (𝑒 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝))) |
67 | 66 | simplbi 493 |
. . . . . . 7
⊢ (𝑒 ∈ 𝐽 → 𝑒 ⊆ 𝑋) |
68 | 67 | ad2antlr 718 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → 𝑒 ⊆ 𝑋) |
69 | 65, 68 | syl5ss 3838 |
. . . . 5
⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ⊆ 𝑋) |
70 | | simplll 791 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝜑) |
71 | | simpllr 793 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ 𝐽) |
72 | 71, 67 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ⊆ 𝑋) |
73 | | simpr 479 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ (𝑒 ∩ 𝑓)) |
74 | 65, 73 | sseldi 3825 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑒) |
75 | 72, 74 | sseldd 3828 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑋) |
76 | 70, 75, 6 | syl2anc 579 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) |
77 | 66 | simprbi 492 |
. . . . . . . . . 10
⊢ (𝑒 ∈ 𝐽 → ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝)) |
78 | 77 | r19.21bi 3141 |
. . . . . . . . 9
⊢ ((𝑒 ∈ 𝐽 ∧ 𝑝 ∈ 𝑒) → 𝑒 ∈ (𝑁‘𝑝)) |
79 | 71, 74, 78 | syl2anc 579 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ (𝑁‘𝑝)) |
80 | | simplr 785 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ 𝐽) |
81 | | inss2 4060 |
. . . . . . . . . 10
⊢ (𝑒 ∩ 𝑓) ⊆ 𝑓 |
82 | 81, 73 | sseldi 3825 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑓) |
83 | 3 | neipeltop 21311 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐽 ↔ (𝑓 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝))) |
84 | 83 | simprbi 492 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐽 → ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝)) |
85 | 84 | r19.21bi 3141 |
. . . . . . . . 9
⊢ ((𝑓 ∈ 𝐽 ∧ 𝑝 ∈ 𝑓) → 𝑓 ∈ (𝑁‘𝑝)) |
86 | 80, 82, 85 | syl2anc 579 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ (𝑁‘𝑝)) |
87 | | fvex 6450 |
. . . . . . . . 9
⊢ (𝑁‘𝑝) ∈ V |
88 | | inelfi 8599 |
. . . . . . . . 9
⊢ (((𝑁‘𝑝) ∈ V ∧ 𝑒 ∈ (𝑁‘𝑝) ∧ 𝑓 ∈ (𝑁‘𝑝)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝))) |
89 | 87, 88 | mp3an1 1576 |
. . . . . . . 8
⊢ ((𝑒 ∈ (𝑁‘𝑝) ∧ 𝑓 ∈ (𝑁‘𝑝)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝))) |
90 | 79, 86, 89 | syl2anc 579 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝))) |
91 | 76, 90 | sseldd 3828 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝)) |
92 | 91 | ralrimiva 3175 |
. . . . 5
⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝)) |
93 | 3 | neipeltop 21311 |
. . . . 5
⊢ ((𝑒 ∩ 𝑓) ∈ 𝐽 ↔ ((𝑒 ∩ 𝑓) ⊆ 𝑋 ∧ ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝))) |
94 | 69, 92, 93 | sylanbrc 578 |
. . . 4
⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ∈ 𝐽) |
95 | 94 | ralrimiva 3175 |
. . 3
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐽) → ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽) |
96 | 95 | ralrimiva 3175 |
. 2
⊢ (𝜑 → ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽) |
97 | | istopg 21077 |
. . 3
⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔
(∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽))) |
98 | 41, 97 | syl 17 |
. 2
⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽))) |
99 | 64, 96, 98 | mpbir2and 704 |
1
⊢ (𝜑 → 𝐽 ∈ Top) |