Step | Hyp | Ref
| Expression |
1 | | pnrmtop 22492 |
. . . 4
⊢ (𝐽 ∈ PNrm → 𝐽 ∈ Top) |
2 | | eqid 2738 |
. . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 |
3 | 2 | opncld 22184 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → (∪ 𝐽 ∖ 𝐴) ∈ (Clsd‘𝐽)) |
4 | 1, 3 | sylan 580 |
. . 3
⊢ ((𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽) → (∪ 𝐽 ∖ 𝐴) ∈ (Clsd‘𝐽)) |
5 | | pnrmcld 22493 |
. . 3
⊢ ((𝐽 ∈ PNrm ∧ (∪ 𝐽
∖ 𝐴) ∈
(Clsd‘𝐽)) →
∃𝑔 ∈ (𝐽 ↑m
ℕ)(∪ 𝐽 ∖ 𝐴) = ∩ ran 𝑔) |
6 | 4, 5 | syldan 591 |
. 2
⊢ ((𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽) → ∃𝑔 ∈ (𝐽 ↑m ℕ)(∪ 𝐽
∖ 𝐴) = ∩ ran 𝑔) |
7 | 1 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) ∧ 𝑥 ∈ ℕ) → 𝐽 ∈ Top) |
8 | | elmapi 8637 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝐽 ↑m ℕ) → 𝑔:ℕ⟶𝐽) |
9 | 8 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) → 𝑔:ℕ⟶𝐽) |
10 | 9 | ffvelrnda 6961 |
. . . . . . . 8
⊢ (((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) ∧ 𝑥 ∈ ℕ) → (𝑔‘𝑥) ∈ 𝐽) |
11 | 2 | opncld 22184 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝑔‘𝑥) ∈ 𝐽) → (∪ 𝐽 ∖ (𝑔‘𝑥)) ∈ (Clsd‘𝐽)) |
12 | 7, 10, 11 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) ∧ 𝑥 ∈ ℕ) → (∪ 𝐽
∖ (𝑔‘𝑥)) ∈ (Clsd‘𝐽)) |
13 | 12 | fmpttd 6989 |
. . . . . 6
⊢ ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) → (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥))):ℕ⟶(Clsd‘𝐽)) |
14 | | fvex 6787 |
. . . . . . 7
⊢
(Clsd‘𝐽)
∈ V |
15 | | nnex 11979 |
. . . . . . 7
⊢ ℕ
∈ V |
16 | 14, 15 | elmap 8659 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥))) ∈ ((Clsd‘𝐽) ↑m ℕ)
↔ (𝑥 ∈ ℕ
↦ (∪ 𝐽 ∖ (𝑔‘𝑥))):ℕ⟶(Clsd‘𝐽)) |
17 | 13, 16 | sylibr 233 |
. . . . 5
⊢ ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) → (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥))) ∈ ((Clsd‘𝐽) ↑m
ℕ)) |
18 | | iundif2 5003 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ ℕ (∪
𝐽 ∖ (𝑔‘𝑥)) = (∪ 𝐽 ∖ ∩ 𝑥 ∈ ℕ (𝑔‘𝑥)) |
19 | | ffn 6600 |
. . . . . . . . 9
⊢ (𝑔:ℕ⟶𝐽 → 𝑔 Fn ℕ) |
20 | | fniinfv 6846 |
. . . . . . . . 9
⊢ (𝑔 Fn ℕ → ∩ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∩ ran 𝑔) |
21 | 9, 19, 20 | 3syl 18 |
. . . . . . . 8
⊢ ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) →
∩ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∩ ran 𝑔) |
22 | 21 | difeq2d 4057 |
. . . . . . 7
⊢ ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) → (∪ 𝐽
∖ ∩ 𝑥 ∈ ℕ (𝑔‘𝑥)) = (∪ 𝐽 ∖ ∩ ran 𝑔)) |
23 | 18, 22 | eqtrid 2790 |
. . . . . 6
⊢ ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) →
∪ 𝑥 ∈ ℕ (∪
𝐽 ∖ (𝑔‘𝑥)) = (∪ 𝐽 ∖ ∩ ran 𝑔)) |
24 | | uniexg 7593 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ PNrm → ∪ 𝐽
∈ V) |
25 | 24 | difexd 5253 |
. . . . . . . . . 10
⊢ (𝐽 ∈ PNrm → (∪ 𝐽
∖ (𝑔‘𝑥)) ∈ V) |
26 | 25 | ralrimivw 3104 |
. . . . . . . . 9
⊢ (𝐽 ∈ PNrm →
∀𝑥 ∈ ℕ
(∪ 𝐽 ∖ (𝑔‘𝑥)) ∈ V) |
27 | 26 | adantr 481 |
. . . . . . . 8
⊢ ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) →
∀𝑥 ∈ ℕ
(∪ 𝐽 ∖ (𝑔‘𝑥)) ∈ V) |
28 | | dfiun2g 4960 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℕ (∪ 𝐽 ∖ (𝑔‘𝑥)) ∈ V → ∪ 𝑥 ∈ ℕ (∪
𝐽 ∖ (𝑔‘𝑥)) = ∪ {𝑓 ∣ ∃𝑥 ∈ ℕ 𝑓 = (∪
𝐽 ∖ (𝑔‘𝑥))}) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) →
∪ 𝑥 ∈ ℕ (∪
𝐽 ∖ (𝑔‘𝑥)) = ∪ {𝑓 ∣ ∃𝑥 ∈ ℕ 𝑓 = (∪
𝐽 ∖ (𝑔‘𝑥))}) |
30 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥))) = (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥))) |
31 | 30 | rnmpt 5864 |
. . . . . . . 8
⊢ ran
(𝑥 ∈ ℕ ↦
(∪ 𝐽 ∖ (𝑔‘𝑥))) = {𝑓 ∣ ∃𝑥 ∈ ℕ 𝑓 = (∪ 𝐽 ∖ (𝑔‘𝑥))} |
32 | 31 | unieqi 4852 |
. . . . . . 7
⊢ ∪ ran (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥))) = ∪ {𝑓
∣ ∃𝑥 ∈
ℕ 𝑓 = (∪ 𝐽
∖ (𝑔‘𝑥))} |
33 | 29, 32 | eqtr4di 2796 |
. . . . . 6
⊢ ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) →
∪ 𝑥 ∈ ℕ (∪
𝐽 ∖ (𝑔‘𝑥)) = ∪ ran (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥)))) |
34 | 23, 33 | eqtr3d 2780 |
. . . . 5
⊢ ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) → (∪ 𝐽
∖ ∩ ran 𝑔) = ∪ ran (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥)))) |
35 | | rneq 5845 |
. . . . . . 7
⊢ (𝑓 = (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥))) → ran 𝑓 = ran (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥)))) |
36 | 35 | unieqd 4853 |
. . . . . 6
⊢ (𝑓 = (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥))) → ∪ ran 𝑓 = ∪ ran (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥)))) |
37 | 36 | rspceeqv 3575 |
. . . . 5
⊢ (((𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥))) ∈ ((Clsd‘𝐽) ↑m ℕ)
∧ (∪ 𝐽 ∖ ∩ ran
𝑔) = ∪ ran (𝑥 ∈ ℕ ↦ (∪ 𝐽
∖ (𝑔‘𝑥)))) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑m
ℕ)(∪ 𝐽 ∖ ∩ ran
𝑔) = ∪ ran 𝑓) |
38 | 17, 34, 37 | syl2anc 584 |
. . . 4
⊢ ((𝐽 ∈ PNrm ∧ 𝑔 ∈ (𝐽 ↑m ℕ)) →
∃𝑓 ∈
((Clsd‘𝐽)
↑m ℕ)(∪ 𝐽 ∖ ∩ ran
𝑔) = ∪ ran 𝑓) |
39 | 38 | ad2ant2r 744 |
. . 3
⊢ (((𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽) ∧ (𝑔 ∈ (𝐽 ↑m ℕ) ∧ (∪ 𝐽
∖ 𝐴) = ∩ ran 𝑔)) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)(∪ 𝐽
∖ ∩ ran 𝑔) = ∪ ran 𝑓) |
40 | | difeq2 4051 |
. . . . . . . 8
⊢ ((∪ 𝐽
∖ 𝐴) = ∩ ran 𝑔 → (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐴)) = (∪ 𝐽
∖ ∩ ran 𝑔)) |
41 | 40 | eqcomd 2744 |
. . . . . . 7
⊢ ((∪ 𝐽
∖ 𝐴) = ∩ ran 𝑔 → (∪ 𝐽 ∖ ∩ ran 𝑔) = (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐴))) |
42 | | elssuni 4871 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽) |
43 | | dfss4 4192 |
. . . . . . . 8
⊢ (𝐴 ⊆ ∪ 𝐽
↔ (∪ 𝐽 ∖ (∪ 𝐽 ∖ 𝐴)) = 𝐴) |
44 | 42, 43 | sylib 217 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐽 → (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐴)) = 𝐴) |
45 | 41, 44 | sylan9eqr 2800 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐽 ∧ (∪ 𝐽 ∖ 𝐴) = ∩ ran 𝑔) → (∪ 𝐽
∖ ∩ ran 𝑔) = 𝐴) |
46 | 45 | ad2ant2l 743 |
. . . . 5
⊢ (((𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽) ∧ (𝑔 ∈ (𝐽 ↑m ℕ) ∧ (∪ 𝐽
∖ 𝐴) = ∩ ran 𝑔)) → (∪ 𝐽 ∖ ∩ ran 𝑔) = 𝐴) |
47 | 46 | eqeq1d 2740 |
. . . 4
⊢ (((𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽) ∧ (𝑔 ∈ (𝐽 ↑m ℕ) ∧ (∪ 𝐽
∖ 𝐴) = ∩ ran 𝑔)) → ((∪
𝐽 ∖ ∩ ran 𝑔) = ∪ ran 𝑓 ↔ 𝐴 = ∪ ran 𝑓)) |
48 | 47 | rexbidv 3226 |
. . 3
⊢ (((𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽) ∧ (𝑔 ∈ (𝐽 ↑m ℕ) ∧ (∪ 𝐽
∖ 𝐴) = ∩ ran 𝑔)) → (∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)(∪ 𝐽
∖ ∩ ran 𝑔) = ∪ ran 𝑓 ↔ ∃𝑓 ∈ ((Clsd‘𝐽) ↑m
ℕ)𝐴 = ∪ ran 𝑓)) |
49 | 39, 48 | mpbid 231 |
. 2
⊢ (((𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽) ∧ (𝑔 ∈ (𝐽 ↑m ℕ) ∧ (∪ 𝐽
∖ 𝐴) = ∩ ran 𝑔)) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)𝐴 = ∪
ran 𝑓) |
50 | 6, 49 | rexlimddv 3220 |
1
⊢ ((𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)𝐴 = ∪
ran 𝑓) |