MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  flimclslem Structured version   Visualization version   GIF version

Theorem flimclslem 23480
Description: Lemma for flimcls 23481. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.)
Hypothesis
Ref Expression
flimcls.2 𝐹 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
Assertion
Ref Expression
flimclslem ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝑆𝐹𝐴 ∈ (𝐽 fLim 𝐹)))

Proof of Theorem flimclslem
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 flimcls.2 . . 3 𝐹 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
2 topontop 22407 . . . . . . . . 9 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
323ad2ant1 1134 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ Top)
4 eqid 2733 . . . . . . . . 9 𝐽 = 𝐽
54neisspw 22603 . . . . . . . 8 (𝐽 ∈ Top → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝐽)
63, 5syl 17 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝐽)
7 toponuni 22408 . . . . . . . . 9 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
873ad2ant1 1134 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋 = 𝐽)
98pweqd 4619 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝒫 𝑋 = 𝒫 𝐽)
106, 9sseqtrrd 4023 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝑋)
11 toponmax 22420 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
12 elpw2g 5344 . . . . . . . . . 10 (𝑋𝐽 → (𝑆 ∈ 𝒫 𝑋𝑆𝑋))
1311, 12syl 17 . . . . . . . . 9 (𝐽 ∈ (TopOn‘𝑋) → (𝑆 ∈ 𝒫 𝑋𝑆𝑋))
1413biimpar 479 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋) → 𝑆 ∈ 𝒫 𝑋)
15143adant3 1133 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ 𝒫 𝑋)
1615snssd 4812 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ⊆ 𝒫 𝑋)
1710, 16unssd 4186 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋)
18 ssun2 4173 . . . . . 6 {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})
19113ad2ant1 1134 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑋𝐽)
20 simp2 1138 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆𝑋)
2119, 20ssexd 5324 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ V)
2221snn0d 4779 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ≠ ∅)
23 ssn0 4400 . . . . . 6 (({𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∧ {𝑆} ≠ ∅) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅)
2418, 22, 23sylancr 588 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅)
2520, 8sseqtrd 4022 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 𝐽)
26 simp3 1139 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
274neindisj 22613 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑆 𝐽) ∧ (𝐴 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥𝑆) ≠ ∅)
2827expr 458 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝑆 𝐽) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑥 ∈ ((nei‘𝐽)‘{𝐴}) → (𝑥𝑆) ≠ ∅))
293, 25, 26, 28syl21anc 837 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑥 ∈ ((nei‘𝐽)‘{𝐴}) → (𝑥𝑆) ≠ ∅))
3029imp 408 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑥𝑆) ≠ ∅)
31 elsni 4645 . . . . . . . . . . 11 (𝑦 ∈ {𝑆} → 𝑦 = 𝑆)
3231ineq2d 4212 . . . . . . . . . 10 (𝑦 ∈ {𝑆} → (𝑥𝑦) = (𝑥𝑆))
3332neeq1d 3001 . . . . . . . . 9 (𝑦 ∈ {𝑆} → ((𝑥𝑦) ≠ ∅ ↔ (𝑥𝑆) ≠ ∅))
3430, 33syl5ibrcom 246 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑦 ∈ {𝑆} → (𝑥𝑦) ≠ ∅))
3534ralrimiv 3146 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑦 ∈ {𝑆} (𝑥𝑦) ≠ ∅)
3635ralrimiva 3147 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥𝑦) ≠ ∅)
37 simp1 1137 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐽 ∈ (TopOn‘𝑋))
384clsss3 22555 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑆 𝐽) → ((cls‘𝐽)‘𝑆) ⊆ 𝐽)
393, 25, 38syl2anc 585 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ⊆ 𝐽)
4039, 26sseldd 3983 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 𝐽)
4140, 8eleqtrrd 2837 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴𝑋)
4241snssd 4812 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝐴} ⊆ 𝑋)
43 snnzg 4778 . . . . . . . . . 10 (𝐴 ∈ ((cls‘𝐽)‘𝑆) → {𝐴} ≠ ∅)
44433ad2ant3 1136 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝐴} ≠ ∅)
45 neifil 23376 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝐴} ⊆ 𝑋 ∧ {𝐴} ≠ ∅) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
4637, 42, 44, 45syl3anc 1372 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
47 filfbas 23344 . . . . . . . 8 (((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
4846, 47syl 17 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
49 ne0i 4334 . . . . . . . . . . 11 (𝐴 ∈ ((cls‘𝐽)‘𝑆) → ((cls‘𝐽)‘𝑆) ≠ ∅)
50493ad2ant3 1136 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ≠ ∅)
51 cls0 22576 . . . . . . . . . . 11 (𝐽 ∈ Top → ((cls‘𝐽)‘∅) = ∅)
523, 51syl 17 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘∅) = ∅)
5350, 52neeqtrrd 3016 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((cls‘𝐽)‘𝑆) ≠ ((cls‘𝐽)‘∅))
54 fveq2 6889 . . . . . . . . . 10 (𝑆 = ∅ → ((cls‘𝐽)‘𝑆) = ((cls‘𝐽)‘∅))
5554necon3i 2974 . . . . . . . . 9 (((cls‘𝐽)‘𝑆) ≠ ((cls‘𝐽)‘∅) → 𝑆 ≠ ∅)
5653, 55syl 17 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ≠ ∅)
57 snfbas 23362 . . . . . . . 8 ((𝑆𝑋𝑆 ≠ ∅ ∧ 𝑋𝐽) → {𝑆} ∈ (fBas‘𝑋))
5820, 56, 19, 57syl3anc 1372 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → {𝑆} ∈ (fBas‘𝑋))
59 fbunfip 23365 . . . . . . 7 ((((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋) ∧ {𝑆} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥𝑦) ≠ ∅))
6048, 58, 59syl2anc 585 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ↔ ∀𝑥 ∈ ((nei‘𝐽)‘{𝐴})∀𝑦 ∈ {𝑆} (𝑥𝑦) ≠ ∅))
6136, 60mpbird 257 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
62 fsubbas 23363 . . . . . 6 (𝑋𝐽 → ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))))
6319, 62syl 17 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))))
6417, 24, 61, 63mpbir3and 1343 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋))
65 fgcl 23374 . . . 4 ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ∈ (Fil‘𝑋))
6664, 65syl 17 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ∈ (Fil‘𝑋))
671, 66eqeltrid 2838 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐹 ∈ (Fil‘𝑋))
68 fvex 6902 . . . . . 6 ((nei‘𝐽)‘{𝐴}) ∈ V
69 snex 5431 . . . . . 6 {𝑆} ∈ V
7068, 69unex 7730 . . . . 5 (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∈ V
71 ssfii 9411 . . . . 5 ((((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ∈ V → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
7270, 71ax-mp 5 . . . 4 (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))
73 ssfg 23368 . . . . . 6 ((fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ∈ (fBas‘𝑋) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))))
7464, 73syl 17 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))))
7574, 1sseqtrrdi 4033 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})) ⊆ 𝐹)
7672, 75sstrid 3993 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ⊆ 𝐹)
77 snssg 4787 . . . . 5 (𝑆 ∈ V → (𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ↔ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
7821, 77syl 17 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}) ↔ {𝑆} ⊆ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))
7918, 78mpbiri 258 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆 ∈ (((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))
8076, 79sseldd 3983 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝑆𝐹)
8176unssad 4187 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)
82 elflim 23467 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))
8337, 67, 82syl2anc 585 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))
8441, 81, 83mpbir2and 712 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 𝐴 ∈ (𝐽 fLim 𝐹))
8567, 80, 843jca 1129 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆𝑋𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝑆𝐹𝐴 ∈ (𝐽 fLim 𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wne 2941  wral 3062  Vcvv 3475  cun 3946  cin 3947  wss 3948  c0 4322  𝒫 cpw 4602  {csn 4628   cuni 4908  cfv 6541  (class class class)co 7406  ficfi 9402  fBascfbas 20925  filGencfg 20926  Topctop 22387  TopOnctopon 22404  clsccl 22514  neicnei 22593  Filcfil 23341   fLim cflim 23430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1o 8463  df-er 8700  df-en 8937  df-fin 8940  df-fi 9403  df-fbas 20934  df-fg 20935  df-top 22388  df-topon 22405  df-cld 22515  df-ntr 22516  df-cls 22517  df-nei 22594  df-fil 23342  df-flim 23435
This theorem is referenced by:  flimcls  23481
  Copyright terms: Public domain W3C validator