Step | Hyp | Ref
| Expression |
1 | | uniss 4394 |
. . . . . . 7
⊢ (𝑒 ⊆ 𝐽 → ∪ 𝑒 ⊆ ∪ 𝐽) |
2 | 1 | adantl 481 |
. . . . . 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 20744 |
. . . . . . 7
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑋 = ∪ 𝐽) |
12 | 2, 11 | sseqtr4d 3605 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ⊆ 𝑋) |
13 | | simp-4l 802 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝜑) |
14 | 12 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ⊆ 𝑋) |
15 | | simpllr 795 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ ∪ 𝑒) |
16 | 14, 15 | sseldd 3569 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑝 ∈ 𝑋) |
17 | 13, 16 | jca 553 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → (𝜑 ∧ 𝑝 ∈ 𝑋)) |
18 | | elssuni 4403 |
. . . . . . . . . 10
⊢ (𝑐 ∈ 𝑒 → 𝑐 ⊆ ∪ 𝑒) |
19 | 18 | ad2antlr 759 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ⊆ ∪ 𝑒) |
20 | 17, 19, 14 | 3jca 1235 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋)) |
21 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ⊆ 𝐽) |
22 | 21 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → 𝑐 ∈ 𝐽) |
23 | 3 | neipeltop 20743 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ 𝐽 ↔ (𝑐 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝))) |
24 | 23 | simprbi 479 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ 𝐽 → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝)) |
25 | 22, 24 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) → ∀𝑝 ∈ 𝑐 𝑐 ∈ (𝑁‘𝑝)) |
26 | 25 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝)) |
27 | 26 | adantllr 751 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → 𝑐 ∈ (𝑁‘𝑝)) |
28 | | sseq1 3589 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑐 → (𝑎 ⊆ ∪ 𝑒 ↔ 𝑐 ⊆ ∪ 𝑒)) |
29 | 28 | 3anbi2d 1396 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋))) |
30 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑐 ∈ (𝑁‘𝑝))) |
31 | 29, 30 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑐 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)))) |
32 | 31 | imbi1d 330 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑐 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))) |
33 | 32 | imbi2d 329 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑐 → (((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) ↔ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))))) |
34 | | ssid 3587 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑋 ⊆ 𝑋 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ⊆ 𝑋) |
36 | 9 | ralrimiva 2949 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝)) |
37 | 3 | neipeltop 20743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ 𝐽 ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝))) |
38 | 35, 36, 37 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ 𝐽) |
39 | | pwexg 4776 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V) |
40 | | rabexg 4739 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 𝑋 ∈
V → {𝑎 ∈
𝒫 𝑋 ∣
∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ∈ V) |
42 | 3, 41 | syl5eqel 2692 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ V) |
43 | 42 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝐽 ∈ V) |
44 | 43, 21 | ssexd 4733 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → 𝑒 ∈ V) |
45 | | uniexg 6853 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ V → ∪ 𝑒
∈ V) |
46 | | sseq2 3590 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = ∪
𝑒 → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ ∪ 𝑒)) |
47 | | sseq1 3589 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = ∪
𝑒 → (𝑏 ⊆ 𝑋 ↔ ∪ 𝑒 ⊆ 𝑋)) |
48 | 46, 47 | 3anbi23d 1394 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = ∪
𝑒 → (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋))) |
49 | 48 | anbi1d 737 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ∪
𝑒 → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)))) |
50 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ∪
𝑒 → (𝑏 ∈ (𝑁‘𝑝) ↔ ∪ 𝑒 ∈ (𝑁‘𝑝))) |
51 | 49, 50 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∪
𝑒 → (((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝)))) |
52 | 51, 5 | vtoclg 3239 |
. . . . . . . . . . 11
⊢ (∪ 𝑒
∈ V → ((((𝜑 ∧
𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) |
53 | 44, 45, 52 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) |
54 | 33, 53 | chvarv 2251 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) |
55 | 54 | ad3antrrr 762 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑐 ⊆ ∪ 𝑒 ∧ ∪ 𝑒
⊆ 𝑋) ∧ 𝑐 ∈ (𝑁‘𝑝)) → ∪ 𝑒 ∈ (𝑁‘𝑝))) |
56 | 20, 27, 55 | mp2and 711 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) ∧ 𝑐 ∈ 𝑒) ∧ 𝑝 ∈ 𝑐) → ∪ 𝑒 ∈ (𝑁‘𝑝)) |
57 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → 𝑝 ∈ ∪ 𝑒) |
58 | | eluni2 4376 |
. . . . . . . 8
⊢ (𝑝 ∈ ∪ 𝑒
↔ ∃𝑐 ∈
𝑒 𝑝 ∈ 𝑐) |
59 | 57, 58 | sylib 207 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∃𝑐 ∈ 𝑒 𝑝 ∈ 𝑐) |
60 | 56, 59 | r19.29a 3060 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐽) ∧ 𝑝 ∈ ∪ 𝑒) → ∪ 𝑒
∈ (𝑁‘𝑝)) |
61 | 60 | ralrimiva 2949 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∀𝑝 ∈ ∪ 𝑒∪
𝑒 ∈ (𝑁‘𝑝)) |
62 | 3 | neipeltop 20743 |
. . . . 5
⊢ (∪ 𝑒
∈ 𝐽 ↔ (∪ 𝑒
⊆ 𝑋 ∧
∀𝑝 ∈ ∪ 𝑒∪ 𝑒 ∈ (𝑁‘𝑝))) |
63 | 12, 61, 62 | sylanbrc 695 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ⊆ 𝐽) → ∪ 𝑒 ∈ 𝐽) |
64 | 63 | ex 449 |
. . 3
⊢ (𝜑 → (𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽)) |
65 | 64 | alrimiv 1842 |
. 2
⊢ (𝜑 → ∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽)) |
66 | | inss1 3795 |
. . . . . 6
⊢ (𝑒 ∩ 𝑓) ⊆ 𝑒 |
67 | 3 | neipeltop 20743 |
. . . . . . . 8
⊢ (𝑒 ∈ 𝐽 ↔ (𝑒 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝))) |
68 | 67 | simplbi 475 |
. . . . . . 7
⊢ (𝑒 ∈ 𝐽 → 𝑒 ⊆ 𝑋) |
69 | 68 | ad2antlr 759 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → 𝑒 ⊆ 𝑋) |
70 | 66, 69 | syl5ss 3579 |
. . . . 5
⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ⊆ 𝑋) |
71 | | simplll 794 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝜑) |
72 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ 𝐽) |
73 | 72, 68 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ⊆ 𝑋) |
74 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ (𝑒 ∩ 𝑓)) |
75 | 66, 74 | sseldi 3566 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑒) |
76 | 73, 75 | sseldd 3569 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑋) |
77 | 71, 76, 6 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) |
78 | 67 | simprbi 479 |
. . . . . . . . . 10
⊢ (𝑒 ∈ 𝐽 → ∀𝑝 ∈ 𝑒 𝑒 ∈ (𝑁‘𝑝)) |
79 | 78 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((𝑒 ∈ 𝐽 ∧ 𝑝 ∈ 𝑒) → 𝑒 ∈ (𝑁‘𝑝)) |
80 | 72, 75, 79 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑒 ∈ (𝑁‘𝑝)) |
81 | | simplr 788 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ 𝐽) |
82 | | inss2 3796 |
. . . . . . . . . 10
⊢ (𝑒 ∩ 𝑓) ⊆ 𝑓 |
83 | 82, 74 | sseldi 3566 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑝 ∈ 𝑓) |
84 | 3 | neipeltop 20743 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐽 ↔ (𝑓 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝))) |
85 | 84 | simprbi 479 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐽 → ∀𝑝 ∈ 𝑓 𝑓 ∈ (𝑁‘𝑝)) |
86 | 85 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((𝑓 ∈ 𝐽 ∧ 𝑝 ∈ 𝑓) → 𝑓 ∈ (𝑁‘𝑝)) |
87 | 81, 83, 86 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → 𝑓 ∈ (𝑁‘𝑝)) |
88 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝑁‘𝑝) ∈ V |
89 | | inelfi 8207 |
. . . . . . . . 9
⊢ (((𝑁‘𝑝) ∈ V ∧ 𝑒 ∈ (𝑁‘𝑝) ∧ 𝑓 ∈ (𝑁‘𝑝)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝))) |
90 | 88, 89 | mp3an1 1403 |
. . . . . . . 8
⊢ ((𝑒 ∈ (𝑁‘𝑝) ∧ 𝑓 ∈ (𝑁‘𝑝)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝))) |
91 | 80, 87, 90 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (fi‘(𝑁‘𝑝))) |
92 | 77, 91 | sseldd 3569 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) ∧ 𝑝 ∈ (𝑒 ∩ 𝑓)) → (𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝)) |
93 | 92 | ralrimiva 2949 |
. . . . 5
⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝)) |
94 | 3 | neipeltop 20743 |
. . . . 5
⊢ ((𝑒 ∩ 𝑓) ∈ 𝐽 ↔ ((𝑒 ∩ 𝑓) ⊆ 𝑋 ∧ ∀𝑝 ∈ (𝑒 ∩ 𝑓)(𝑒 ∩ 𝑓) ∈ (𝑁‘𝑝))) |
95 | 70, 93, 94 | sylanbrc 695 |
. . . 4
⊢ (((𝜑 ∧ 𝑒 ∈ 𝐽) ∧ 𝑓 ∈ 𝐽) → (𝑒 ∩ 𝑓) ∈ 𝐽) |
96 | 95 | ralrimiva 2949 |
. . 3
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐽) → ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽) |
97 | 96 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽) |
98 | | istopg 20525 |
. . 3
⊢ (𝐽 ∈ V → (𝐽 ∈ Top ↔
(∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽))) |
99 | 42, 98 | syl 17 |
. 2
⊢ (𝜑 → (𝐽 ∈ Top ↔ (∀𝑒(𝑒 ⊆ 𝐽 → ∪ 𝑒 ∈ 𝐽) ∧ ∀𝑒 ∈ 𝐽 ∀𝑓 ∈ 𝐽 (𝑒 ∩ 𝑓) ∈ 𝐽))) |
100 | 65, 97, 99 | mpbir2and 959 |
1
⊢ (𝜑 → 𝐽 ∈ Top) |