| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nrmtop 23344 | . . 3
⊢ (𝐽 ∈ Nrm → 𝐽 ∈ Top) | 
| 2 | 1 | adantr 480 | . 2
⊢ ((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
→ 𝐽 ∈
Top) | 
| 3 |  | simpll 767 | . . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ Nrm) | 
| 4 |  | simprl 771 | . . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝐽) | 
| 5 | 2 | adantr 480 | . . . . . . 7
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ Top) | 
| 6 |  | toptopon2 22924 | . . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) | 
| 7 | 5, 6 | sylib 218 | . . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ (TopOn‘∪ 𝐽)) | 
| 8 |  | simplr 769 | . . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (KQ‘𝐽) ∈ Fre) | 
| 9 |  | simprr 773 | . . . . . . 7
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑥) | 
| 10 |  | elunii 4912 | . . . . . . 7
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐽) → 𝑦 ∈ ∪ 𝐽) | 
| 11 | 9, 4, 10 | syl2anc 584 | . . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ ∪ 𝐽) | 
| 12 |  | eqid 2737 | . . . . . . 7
⊢ (𝑧 ∈ ∪ 𝐽
↦ {𝑤 ∈ 𝐽 ∣ 𝑧 ∈ 𝑤}) = (𝑧 ∈ ∪ 𝐽 ↦ {𝑤 ∈ 𝐽 ∣ 𝑧 ∈ 𝑤}) | 
| 13 | 12 | r0cld 23746 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ (KQ‘𝐽) ∈
Fre ∧ 𝑦 ∈ ∪ 𝐽)
→ {𝑎 ∈ ∪ 𝐽
∣ ∀𝑏 ∈
𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ∈ (Clsd‘𝐽)) | 
| 14 | 7, 8, 11, 13 | syl3anc 1373 | . . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ∈ (Clsd‘𝐽)) | 
| 15 |  | simp1rr 1240 | . . . . . . 7
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) → 𝑦 ∈ 𝑥) | 
| 16 | 4 | adantr 480 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽) → 𝑥 ∈ 𝐽) | 
| 17 |  | elequ2 2123 | . . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → (𝑎 ∈ 𝑏 ↔ 𝑎 ∈ 𝑥)) | 
| 18 |  | elequ2 2123 | . . . . . . . . . . 11
⊢ (𝑏 = 𝑥 → (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑥)) | 
| 19 | 17, 18 | bibi12d 345 | . . . . . . . . . 10
⊢ (𝑏 = 𝑥 → ((𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) ↔ (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))) | 
| 20 | 19 | rspcv 3618 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐽 → (∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) → (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))) | 
| 21 | 16, 20 | syl 17 | . . . . . . . 8
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽) → (∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) → (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))) | 
| 22 | 21 | 3impia 1118 | . . . . . . 7
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) → (𝑎 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) | 
| 23 | 15, 22 | mpbird 257 | . . . . . 6
⊢ ((((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) ∧ 𝑎 ∈ ∪ 𝐽 ∧ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) → 𝑎 ∈ 𝑥) | 
| 24 | 23 | rabssdv 4075 | . . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑥) | 
| 25 |  | nrmsep3 23363 | . . . . 5
⊢ ((𝐽 ∈ Nrm ∧ (𝑥 ∈ 𝐽 ∧ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ∈ (Clsd‘𝐽) ∧ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑥)) → ∃𝑧 ∈ 𝐽 ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) | 
| 26 | 3, 4, 14, 24, 25 | syl13anc 1374 | . . . 4
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∃𝑧 ∈ 𝐽 ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) | 
| 27 |  | elequ1 2115 | . . . . . . . . . 10
⊢ (𝑎 = 𝑦 → (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) | 
| 28 | 27 | bibi1d 343 | . . . . . . . . 9
⊢ (𝑎 = 𝑦 → ((𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) ↔ (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏))) | 
| 29 | 28 | ralbidv 3178 | . . . . . . . 8
⊢ (𝑎 = 𝑦 → (∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏) ↔ ∀𝑏 ∈ 𝐽 (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏))) | 
| 30 |  | biidd 262 | . . . . . . . . 9
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) | 
| 31 | 30 | ralrimivw 3150 | . . . . . . . 8
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∀𝑏 ∈ 𝐽 (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)) | 
| 32 | 29, 11, 31 | elrabd 3694 | . . . . . . 7
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)}) | 
| 33 |  | ssel 3977 | . . . . . . 7
⊢ ({𝑎 ∈ ∪ 𝐽
∣ ∀𝑏 ∈
𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 → (𝑦 ∈ {𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} → 𝑦 ∈ 𝑧)) | 
| 34 | 32, 33 | syl5com 31 | . . . . . 6
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 → 𝑦 ∈ 𝑧)) | 
| 35 | 34 | anim1d 611 | . . . . 5
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥) → (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))) | 
| 36 | 35 | reximdv 3170 | . . . 4
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (∃𝑧 ∈ 𝐽 ({𝑎 ∈ ∪ 𝐽 ∣ ∀𝑏 ∈ 𝐽 (𝑎 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏)} ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥) → ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))) | 
| 37 | 26, 36 | mpd 15 | . . 3
⊢ (((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) | 
| 38 | 37 | ralrimivva 3202 | . 2
⊢ ((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
→ ∀𝑥 ∈
𝐽 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)) | 
| 39 |  | isreg 23340 | . 2
⊢ (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥))) | 
| 40 | 2, 38, 39 | sylanbrc 583 | 1
⊢ ((𝐽 ∈ Nrm ∧
(KQ‘𝐽) ∈ Fre)
→ 𝐽 ∈
Reg) |