Step | Hyp | Ref
| Expression |
1 | | nrmtop 20950 |
. . 3
⊢ (𝐽 ∈ Nrm → 𝐽 ∈ Top) |
2 | 1 | adantr 480 |
. 2
⊢ ((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
→ 𝐽 ∈
Top) |
3 | | simpll 786 |
. . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ Nrm) |
4 | | simprl 790 |
. . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝐽) |
5 | 2 | adantr 480 |
. . . . . . 7
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ Top) |
6 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 |
7 | 6 | toptopon 20548 |
. . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
8 | 5, 7 | sylib 207 |
. . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
9 | | simplr 788 |
. . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (KQ‘𝐽) ∈ Fre) |
10 | | simprr 792 |
. . . . . . 7
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑥) |
11 | | elunii 4377 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐽) → 𝑦 ∈ ∪ 𝐽) |
12 | 10, 4, 11 | syl2anc 691 |
. . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ ∪ 𝐽) |
13 | | eqid 2610 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ 𝐽
↦ {𝑤 ∈ 𝐽 ∣ 𝑧 ∈ 𝑤}) = (𝑧 ∈ ∪ 𝐽 ↦ {𝑤 ∈ 𝐽 ∣ 𝑧 ∈ 𝑤}) |
14 | 13 | r0cld 21351 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ (KQ‘𝐽) ∈
Fre ∧ 𝑦 ∈ ∪ 𝐽)
→ {𝑎 ∈ ∪ 𝐽
∣ ∀𝑏 ∈
𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ∈ (Clsd‘𝐽)) |
15 | 8, 9, 12, 14 | syl3anc 1318 |
. . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ∈ (Clsd‘𝐽)) |
16 | | simp1rr 1120 |
. . . . . . 7
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) → 𝑦 ∈ 𝑥) |
17 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽) → 𝑥 ∈ 𝐽) |
18 | | elequ2 1991 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → (𝑎 ∈ 𝑏 ↔ 𝑎 ∈ 𝑥)) |
19 | | elequ2 1991 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑥)) |
20 | 18, 19 | bibi12d 334 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑥 → ((𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) ↔ (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))) |
21 | 20 | rspcv 3278 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐽 → (∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) → (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))) |
22 | 17, 21 | syl 17 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽) → (∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) → (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))) |
23 | 22 | 3impia 1253 |
. . . . . . 7
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) → (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
24 | 16, 23 | mpbird 246 |
. . . . . 6
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) → 𝑎 ∈ 𝑥) |
25 | 24 | rabssdv 3645 |
. . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑥) |
26 | | nrmsep3 20969 |
. . . . 5
⊢ ((𝐽 ∈ Nrm ∧ (𝑥 ∈ 𝐽 ∧ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ∈ (Clsd‘𝐽) ∧ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑥)) → ∃𝑧 ∈ 𝐽 ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) |
27 | 3, 4, 15, 25, 26 | syl13anc 1320 |
. . . 4
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∃𝑧 ∈ 𝐽 ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) |
28 | | biidd 251 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) |
29 | 28 | ralrimivw 2950 |
. . . . . . . 8
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∀𝑏 ∈ 𝐽 (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) |
30 | | elequ1 1984 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑦 → (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) |
31 | 30 | bibi1d 332 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑦 → ((𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) ↔ (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏))) |
32 | 31 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑎 = 𝑦 → (∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) ↔ ∀𝑏 ∈ 𝐽 (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏))) |
33 | 32 | elrab 3331 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ↔ (𝑦 ∈ ∪ 𝐽 ∧ ∀𝑏 ∈ 𝐽 (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏))) |
34 | 12, 29, 33 | sylanbrc 695 |
. . . . . . 7
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)}) |
35 | | ssel 3562 |
. . . . . . 7
⊢ ({𝑎 ∈ ∪ 𝐽
∣ ∀𝑏 ∈
𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 → (𝑦 ∈ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} → 𝑦 ∈ 𝑧)) |
36 | 34, 35 | syl5com 31 |
. . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 → 𝑦 ∈ 𝑧)) |
37 | 36 | anim1d 586 |
. . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥) → (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))) |
38 | 37 | reximdv 2999 |
. . . 4
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (∃𝑧 ∈ 𝐽 ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥) → ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))) |
39 | 27, 38 | mpd 15 |
. . 3
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) |
40 | 39 | ralrimivva 2954 |
. 2
⊢ ((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
→ ∀𝑥 ∈
𝐽 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) |
41 | | isreg 20946 |
. 2
⊢ (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))) |
42 | 2, 40, 41 | sylanbrc 695 |
1
⊢ ((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
→ 𝐽 ∈
Reg) |