Step | Hyp | Ref
| Expression |
1 | | 1stctop 21246 |
. 2
⊢ (𝐽 ∈ 1st𝜔
→ 𝐽 ∈
Top) |
2 | | difss 3737 |
. . . . . . . . . 10
⊢ (∪ 𝐽
∖ 𝑥) ⊆ ∪ 𝐽 |
3 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ∪ 𝐽 =
∪ 𝐽 |
4 | 3 | 1stcelcls 21264 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 1st𝜔
∧ (∪ 𝐽 ∖ 𝑥) ⊆ ∪ 𝐽) → (𝑦 ∈ ((cls‘𝐽)‘(∪ 𝐽 ∖ 𝑥)) ↔ ∃𝑓(𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦))) |
5 | 2, 4 | mpan2 707 |
. . . . . . . . 9
⊢ (𝐽 ∈ 1st𝜔
→ (𝑦 ∈
((cls‘𝐽)‘(∪ 𝐽
∖ 𝑥)) ↔
∃𝑓(𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦))) |
6 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ (𝑦 ∈
((cls‘𝐽)‘(∪ 𝐽
∖ 𝑥)) ↔
∃𝑓(𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦))) |
7 | 1 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ 𝐽 ∈
Top) |
8 | 7 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝐽 ∈ Top) |
9 | 3 | toptopon 20722 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
10 | 8, 9 | sylib 208 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
11 | | simprr 796 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑓(⇝𝑡‘𝐽)𝑦) |
12 | | lmcl 21101 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝑓(⇝𝑡‘𝐽)𝑦) → 𝑦 ∈ ∪ 𝐽) |
13 | 10, 11, 12 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑦 ∈ ∪ 𝐽) |
14 | | nnuz 11723 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) |
15 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
16 | 15 | rnex 7100 |
. . . . . . . . . . . . . . . 16
⊢ ran 𝑓 ∈ V |
17 | | snex 4908 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦} ∈ V |
18 | 16, 17 | unex 6956 |
. . . . . . . . . . . . . . 15
⊢ (ran
𝑓 ∪ {𝑦}) ∈ V |
19 | | resttop 20964 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ (ran 𝑓 ∪ {𝑦}) ∈ V) → (𝐽 ↾t (ran 𝑓 ∪ {𝑦})) ∈ Top) |
20 | 8, 18, 19 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → (𝐽 ↾t (ran 𝑓 ∪ {𝑦})) ∈ Top) |
21 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ ∪ (𝐽
↾t (ran 𝑓
∪ {𝑦})) = ∪ (𝐽
↾t (ran 𝑓
∪ {𝑦})) |
22 | 21 | toptopon 20722 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ↾t (ran 𝑓 ∪ {𝑦})) ∈ Top ↔ (𝐽 ↾t (ran 𝑓 ∪ {𝑦})) ∈ (TopOn‘∪ (𝐽
↾t (ran 𝑓
∪ {𝑦})))) |
23 | 20, 22 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → (𝐽 ↾t (ran 𝑓 ∪ {𝑦})) ∈ (TopOn‘∪ (𝐽
↾t (ran 𝑓
∪ {𝑦})))) |
24 | | 1zzd 11408 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 1 ∈ ℤ) |
25 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ↾t (ran 𝑓 ∪ {𝑦})) = (𝐽 ↾t (ran 𝑓 ∪ {𝑦})) |
26 | 18 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → (ran 𝑓 ∪ {𝑦}) ∈ V) |
27 | | ssun2 3777 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑦} ⊆ (ran 𝑓 ∪ {𝑦}) |
28 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
29 | 28 | snss 4316 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (ran 𝑓 ∪ {𝑦}) ↔ {𝑦} ⊆ (ran 𝑓 ∪ {𝑦})) |
30 | 27, 29 | mpbir 221 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ (ran 𝑓 ∪ {𝑦}) |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑦 ∈ (ran 𝑓 ∪ {𝑦})) |
32 | | ffn 6045 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:ℕ⟶(∪ 𝐽
∖ 𝑥) → 𝑓 Fn ℕ) |
33 | 32 | ad2antrl 764 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑓 Fn ℕ) |
34 | | dffn3 6054 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 Fn ℕ ↔ 𝑓:ℕ⟶ran 𝑓) |
35 | 33, 34 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑓:ℕ⟶ran 𝑓) |
36 | | ssun1 3776 |
. . . . . . . . . . . . . . . 16
⊢ ran 𝑓 ⊆ (ran 𝑓 ∪ {𝑦}) |
37 | | fss 6056 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:ℕ⟶ran 𝑓 ∧ ran 𝑓 ⊆ (ran 𝑓 ∪ {𝑦})) → 𝑓:ℕ⟶(ran 𝑓 ∪ {𝑦})) |
38 | 35, 36, 37 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑓:ℕ⟶(ran 𝑓 ∪ {𝑦})) |
39 | 25, 14, 26, 8, 31, 24, 38 | lmss 21102 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → (𝑓(⇝𝑡‘𝐽)𝑦 ↔ 𝑓(⇝𝑡‘(𝐽 ↾t (ran 𝑓 ∪ {𝑦})))𝑦)) |
40 | 11, 39 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑓(⇝𝑡‘(𝐽 ↾t (ran 𝑓 ∪ {𝑦})))𝑦) |
41 | 38 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ (ran 𝑓 ∪ {𝑦})) |
42 | | simprl 794 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥)) |
43 | 42 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ (∪ 𝐽 ∖ 𝑥)) |
44 | 43 | eldifbd 3587 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) ∧ 𝑘 ∈ ℕ) → ¬ (𝑓‘𝑘) ∈ 𝑥) |
45 | 41, 44 | eldifd 3585 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ ((ran 𝑓 ∪ {𝑦}) ∖ 𝑥)) |
46 | | difin 3861 |
. . . . . . . . . . . . . . 15
⊢ ((ran
𝑓 ∪ {𝑦}) ∖ ((ran 𝑓 ∪ {𝑦}) ∩ 𝑥)) = ((ran 𝑓 ∪ {𝑦}) ∖ 𝑥) |
47 | | frn 6053 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓:ℕ⟶(∪ 𝐽
∖ 𝑥) → ran 𝑓 ⊆ (∪ 𝐽
∖ 𝑥)) |
48 | 47 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → ran 𝑓 ⊆ (∪ 𝐽 ∖ 𝑥)) |
49 | 48 | difss2d 3740 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → ran 𝑓 ⊆ ∪ 𝐽) |
50 | 13 | snssd 4340 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → {𝑦} ⊆ ∪ 𝐽) |
51 | 49, 50 | unssd 3789 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → (ran 𝑓 ∪ {𝑦}) ⊆ ∪ 𝐽) |
52 | 3 | restuni 20966 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ (ran 𝑓 ∪ {𝑦}) ⊆ ∪ 𝐽) → (ran 𝑓 ∪ {𝑦}) = ∪ (𝐽 ↾t (ran 𝑓 ∪ {𝑦}))) |
53 | 8, 51, 52 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → (ran 𝑓 ∪ {𝑦}) = ∪ (𝐽 ↾t (ran 𝑓 ∪ {𝑦}))) |
54 | 53 | difeq1d 3727 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → ((ran 𝑓 ∪ {𝑦}) ∖ ((ran 𝑓 ∪ {𝑦}) ∩ 𝑥)) = (∪ (𝐽 ↾t (ran 𝑓 ∪ {𝑦})) ∖ ((ran 𝑓 ∪ {𝑦}) ∩ 𝑥))) |
55 | 46, 54 | syl5eqr 2670 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → ((ran 𝑓 ∪ {𝑦}) ∖ 𝑥) = (∪ (𝐽 ↾t (ran 𝑓 ∪ {𝑦})) ∖ ((ran 𝑓 ∪ {𝑦}) ∩ 𝑥))) |
56 | | incom 3805 |
. . . . . . . . . . . . . . . 16
⊢ ((ran
𝑓 ∪ {𝑦}) ∩ 𝑥) = (𝑥 ∩ (ran 𝑓 ∪ {𝑦})) |
57 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑥 ∈ (𝑘Gen‘𝐽)) |
58 | | fss 6056 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:ℕ⟶(∪ 𝐽
∖ 𝑥) ∧ (∪ 𝐽
∖ 𝑥) ⊆ ∪ 𝐽)
→ 𝑓:ℕ⟶∪
𝐽) |
59 | 42, 2, 58 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑓:ℕ⟶∪
𝐽) |
60 | 10, 59, 11 | 1stckgenlem 21356 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → (𝐽 ↾t (ran 𝑓 ∪ {𝑦})) ∈ Comp) |
61 | | kgeni 21340 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t (ran 𝑓
∪ {𝑦})) ∈ Comp)
→ (𝑥 ∩ (ran 𝑓 ∪ {𝑦})) ∈ (𝐽 ↾t (ran 𝑓 ∪ {𝑦}))) |
62 | 57, 60, 61 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → (𝑥 ∩ (ran 𝑓 ∪ {𝑦})) ∈ (𝐽 ↾t (ran 𝑓 ∪ {𝑦}))) |
63 | 56, 62 | syl5eqel 2705 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → ((ran 𝑓 ∪ {𝑦}) ∩ 𝑥) ∈ (𝐽 ↾t (ran 𝑓 ∪ {𝑦}))) |
64 | 21 | opncld 20837 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ↾t (ran 𝑓 ∪ {𝑦})) ∈ Top ∧ ((ran 𝑓 ∪ {𝑦}) ∩ 𝑥) ∈ (𝐽 ↾t (ran 𝑓 ∪ {𝑦}))) → (∪
(𝐽 ↾t (ran
𝑓 ∪ {𝑦})) ∖ ((ran 𝑓 ∪ {𝑦}) ∩ 𝑥)) ∈ (Clsd‘(𝐽 ↾t (ran 𝑓 ∪ {𝑦})))) |
65 | 20, 63, 64 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → (∪
(𝐽 ↾t (ran
𝑓 ∪ {𝑦})) ∖ ((ran 𝑓 ∪ {𝑦}) ∩ 𝑥)) ∈ (Clsd‘(𝐽 ↾t (ran 𝑓 ∪ {𝑦})))) |
66 | 55, 65 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → ((ran 𝑓 ∪ {𝑦}) ∖ 𝑥) ∈ (Clsd‘(𝐽 ↾t (ran 𝑓 ∪ {𝑦})))) |
67 | 14, 23, 24, 40, 45, 66 | lmcld 21107 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑦 ∈ ((ran 𝑓 ∪ {𝑦}) ∖ 𝑥)) |
68 | 67 | eldifbd 3587 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → ¬ 𝑦 ∈ 𝑥) |
69 | 13, 68 | eldifd 3585 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
∧ (𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦)) → 𝑦 ∈ (∪ 𝐽 ∖ 𝑥)) |
70 | 69 | ex 450 |
. . . . . . . . 9
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ ((𝑓:ℕ⟶(∪
𝐽 ∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦) → 𝑦 ∈ (∪ 𝐽 ∖ 𝑥))) |
71 | 70 | exlimdv 1861 |
. . . . . . . 8
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ (∃𝑓(𝑓:ℕ⟶(∪ 𝐽
∖ 𝑥) ∧ 𝑓(⇝𝑡‘𝐽)𝑦) → 𝑦 ∈ (∪ 𝐽 ∖ 𝑥))) |
72 | 6, 71 | sylbid 230 |
. . . . . . 7
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ (𝑦 ∈
((cls‘𝐽)‘(∪ 𝐽
∖ 𝑥)) → 𝑦 ∈ (∪ 𝐽
∖ 𝑥))) |
73 | 72 | ssrdv 3609 |
. . . . . 6
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ ((cls‘𝐽)‘(∪ 𝐽 ∖ 𝑥)) ⊆ (∪
𝐽 ∖ 𝑥)) |
74 | 3 | iscld4 20869 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (∪ 𝐽
∖ 𝑥) ⊆ ∪ 𝐽)
→ ((∪ 𝐽 ∖ 𝑥) ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘(∪ 𝐽 ∖ 𝑥)) ⊆ (∪
𝐽 ∖ 𝑥))) |
75 | 7, 2, 74 | sylancl 694 |
. . . . . 6
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ ((∪ 𝐽 ∖ 𝑥) ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘(∪ 𝐽 ∖ 𝑥)) ⊆ (∪
𝐽 ∖ 𝑥))) |
76 | 73, 75 | mpbird 247 |
. . . . 5
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ (∪ 𝐽 ∖ 𝑥) ∈ (Clsd‘𝐽)) |
77 | | elssuni 4467 |
. . . . . . . 8
⊢ (𝑥 ∈
(𝑘Gen‘𝐽)
→ 𝑥 ⊆ ∪ (𝑘Gen‘𝐽)) |
78 | 77 | adantl 482 |
. . . . . . 7
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ 𝑥 ⊆ ∪ (𝑘Gen‘𝐽)) |
79 | 3 | kgenuni 21342 |
. . . . . . . 8
⊢ (𝐽 ∈ Top → ∪ 𝐽 =
∪ (𝑘Gen‘𝐽)) |
80 | 7, 79 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ ∪ 𝐽 = ∪
(𝑘Gen‘𝐽)) |
81 | 78, 80 | sseqtr4d 3642 |
. . . . . 6
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ 𝑥 ⊆ ∪ 𝐽) |
82 | 3 | isopn2 20836 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽)
→ (𝑥 ∈ 𝐽 ↔ (∪ 𝐽
∖ 𝑥) ∈
(Clsd‘𝐽))) |
83 | 7, 81, 82 | syl2anc 693 |
. . . . 5
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ (𝑥 ∈ 𝐽 ↔ (∪ 𝐽
∖ 𝑥) ∈
(Clsd‘𝐽))) |
84 | 76, 83 | mpbird 247 |
. . . 4
⊢ ((𝐽 ∈ 1st𝜔
∧ 𝑥 ∈
(𝑘Gen‘𝐽))
→ 𝑥 ∈ 𝐽) |
85 | 84 | ex 450 |
. . 3
⊢ (𝐽 ∈ 1st𝜔
→ (𝑥 ∈
(𝑘Gen‘𝐽)
→ 𝑥 ∈ 𝐽)) |
86 | 85 | ssrdv 3609 |
. 2
⊢ (𝐽 ∈ 1st𝜔
→ (𝑘Gen‘𝐽) ⊆ 𝐽) |
87 | | iskgen2 21351 |
. 2
⊢ (𝐽 ∈ ran 𝑘Gen ↔
(𝐽 ∈ Top ∧
(𝑘Gen‘𝐽)
⊆ 𝐽)) |
88 | 1, 86, 87 | sylanbrc 698 |
1
⊢ (𝐽 ∈ 1st𝜔
→ 𝐽 ∈ ran
𝑘Gen) |