Step | Hyp | Ref
| Expression |
1 | | nrmtop 22683 |
. . 3
⊢ (𝐽 ∈ Nrm → 𝐽 ∈ Top) |
2 | 1 | adantr 481 |
. 2
⊢ ((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
→ 𝐽 ∈
Top) |
3 | | simpll 765 |
. . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ Nrm) |
4 | | simprl 769 |
. . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝐽) |
5 | 2 | adantr 481 |
. . . . . . 7
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ Top) |
6 | | toptopon2 22263 |
. . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
7 | 5, 6 | sylib 217 |
. . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
8 | | simplr 767 |
. . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (KQ‘𝐽) ∈ Fre) |
9 | | simprr 771 |
. . . . . . 7
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑥) |
10 | | elunii 4869 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐽) → 𝑦 ∈ ∪ 𝐽) |
11 | 9, 4, 10 | syl2anc 584 |
. . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ ∪ 𝐽) |
12 | | eqid 2736 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ 𝐽
↦ {𝑤 ∈ 𝐽 ∣ 𝑧 ∈ 𝑤}) = (𝑧 ∈ ∪ 𝐽 ↦ {𝑤 ∈ 𝐽 ∣ 𝑧 ∈ 𝑤}) |
13 | 12 | r0cld 23085 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ (KQ‘𝐽) ∈
Fre ∧ 𝑦 ∈ ∪ 𝐽)
→ {𝑎 ∈ ∪ 𝐽
∣ ∀𝑏 ∈
𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ∈ (Clsd‘𝐽)) |
14 | 7, 8, 11, 13 | syl3anc 1371 |
. . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ∈ (Clsd‘𝐽)) |
15 | | simp1rr 1239 |
. . . . . . 7
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) → 𝑦 ∈ 𝑥) |
16 | 4 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽) → 𝑥 ∈ 𝐽) |
17 | | elequ2 2121 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → (𝑎 ∈ 𝑏 ↔ 𝑎 ∈ 𝑥)) |
18 | | elequ2 2121 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑥)) |
19 | 17, 18 | bibi12d 345 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑥 → ((𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) ↔ (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))) |
20 | 19 | rspcv 3576 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐽 → (∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) → (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))) |
21 | 16, 20 | syl 17 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽) → (∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) → (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))) |
22 | 21 | 3impia 1117 |
. . . . . . 7
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) → (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
23 | 15, 22 | mpbird 256 |
. . . . . 6
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) → 𝑎 ∈ 𝑥) |
24 | 23 | rabssdv 4031 |
. . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑥) |
25 | | nrmsep3 22702 |
. . . . 5
⊢ ((𝐽 ∈ Nrm ∧ (𝑥 ∈ 𝐽 ∧ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ∈ (Clsd‘𝐽) ∧ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑥)) → ∃𝑧 ∈ 𝐽 ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) |
26 | 3, 4, 14, 24, 25 | syl13anc 1372 |
. . . 4
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∃𝑧 ∈ 𝐽 ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) |
27 | | elequ1 2113 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑦 → (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) |
28 | 27 | bibi1d 343 |
. . . . . . . . 9
⊢ (𝑎 = 𝑦 → ((𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) ↔ (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏))) |
29 | 28 | ralbidv 3173 |
. . . . . . . 8
⊢ (𝑎 = 𝑦 → (∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) ↔ ∀𝑏 ∈ 𝐽 (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏))) |
30 | | biidd 261 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) |
31 | 30 | ralrimivw 3146 |
. . . . . . . 8
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∀𝑏 ∈ 𝐽 (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) |
32 | 29, 11, 31 | elrabd 3646 |
. . . . . . 7
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)}) |
33 | | ssel 3936 |
. . . . . . 7
⊢ ({𝑎 ∈ ∪ 𝐽
∣ ∀𝑏 ∈
𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 → (𝑦 ∈ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} → 𝑦 ∈ 𝑧)) |
34 | 32, 33 | syl5com 31 |
. . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 → 𝑦 ∈ 𝑧)) |
35 | 34 | anim1d 611 |
. . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥) → (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))) |
36 | 35 | reximdv 3166 |
. . . 4
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (∃𝑧 ∈ 𝐽 ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥) → ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))) |
37 | 26, 36 | mpd 15 |
. . 3
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) |
38 | 37 | ralrimivva 3196 |
. 2
⊢ ((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
→ ∀𝑥 ∈
𝐽 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) |
39 | | isreg 22679 |
. 2
⊢ (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))) |
40 | 2, 38, 39 | sylanbrc 583 |
1
⊢ ((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
→ 𝐽 ∈
Reg) |