hausflim - Metamath Proof Explorer

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

Theorem hausflim 23959

Description: A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)

**Hypothesis**
Ref	Expression
flimcf.1	⊢ 𝑋 = ∪ 𝐽

**Assertion**
Ref	Expression
hausflim	⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))

Distinct variable groups: 𝑥,𝑓,𝐽 𝑓,𝑋,𝑥

Proof of Theorem hausflim Dummy variables 𝑣 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		haustop 23309	. . 3 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
2		hausflimi 23958	. . . 4 ⊢ (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
3	2	ralrimivw 3134	. . 3 ⊢ (𝐽 ∈ Haus → ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
4	1, 3	jca 511	. 2 ⊢ (𝐽 ∈ Haus → (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
5		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝐽 ∈ Top)
6		flimcf.1	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = ∪ 𝐽
7	6	toptopon 22895	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
8	5, 7	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝐽 ∈ (TopOn‘𝑋))
9		simprll 779	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑧 ∈ 𝑋)
10	9	snssd 4753	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑧} ⊆ 𝑋)
11	9	snn0d 4720	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑧} ≠ ∅)
12		neifil 23858	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑧} ⊆ 𝑋 ∧ {𝑧} ≠ ∅) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
13	8, 10, 11, 12	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
14		filfbas 23826	. . . . . . . . . . . 12 ⊢ (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
15	13, 14	syl 17	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
16		simprlr 780	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑤 ∈ 𝑋)
17	16	snssd 4753	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑤} ⊆ 𝑋)
18	16	snn0d 4720	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑤} ≠ ∅)
19		neifil 23858	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑤} ⊆ 𝑋 ∧ {𝑤} ≠ ∅) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
20	8, 17, 18, 19	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
21		filfbas 23826	. . . . . . . . . . . 12 ⊢ (((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
23		fbunfip 23847	. . . . . . . . . . 11 ⊢ ((((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋) ∧ ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅))
24	15, 22, 23	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅))
25	6	neisspw 23085	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑧}) ⊆ 𝒫 𝑋)
26	6	neisspw 23085	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑤}) ⊆ 𝒫 𝑋)
27	25, 26	unssd 4133	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋)
28	27	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋)
29	28	a1d 25	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋))
30		ssun1 4119	. . . . . . . . . . . . . 14 ⊢ ((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))
31		filn0 23840	. . . . . . . . . . . . . . 15 ⊢ (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
32	13, 31	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
33		ssn0 4345	. . . . . . . . . . . . . 14 ⊢ ((((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∧ ((nei‘𝐽)‘{𝑧}) ≠ ∅) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅)
34	30, 32, 33	sylancr 588	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅)
35	34	a1d 25	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅))
36		idd 24	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
37	29, 35, 36	3jcad 1130	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
38	6	topopn 22884	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
39	38	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑋 ∈ 𝐽)
40		fsubbas 23845	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝐽 → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
41	39, 40	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
42		fgcl 23856	. . . . . . . . . . . . . . 15 ⊢ ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋))
43	42	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋))
44		simplrr 778	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ≠ 𝑤)
45	9	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ∈ 𝑋)
46	16	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑤 ∈ 𝑋)
47		fvex 6848	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((nei‘𝐽)‘{𝑧}) ∈ V
48		fvex 6848	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((nei‘𝐽)‘{𝑤}) ∈ V
49	47, 48	unex 7692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V
50		ssfii 9326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))
51	49, 50	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))
52		ssfg 23850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
53	52	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
54	51, 53	sstrid 3934	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
55	30, 54	sstrid 3934	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
56	8	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
57		elflim 23949	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
58	56, 43, 57	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
59	45, 55, 58	mpbir2and 714	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
60	54	unssbd 4135	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
61		elflim 23949	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
62	56, 43, 61	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
63	46, 60, 62	mpbir2and 714	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
64		eleq1w 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
65		eleq1w 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
66	64, 65	moi 3665	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → 𝑧 = 𝑤)
67	66	3com23 1127	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → 𝑧 = 𝑤)
68	67	3expia 1122	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
69	45, 46, 59, 63, 68	syl22anc 839	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
70	69	necon3ad 2946	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑧 ≠ 𝑤 → ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
71	44, 70	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
72		oveq2 7369	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝐽 fLim 𝑓) = (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
73	72	eleq2d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝑥 ∈ (𝐽 fLim 𝑓) ↔ 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
74	73	mobidv 2550	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ∃𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
75	74	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (¬ ∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
76	75	rspcev 3565	. . . . . . . . . . . . . 14 ⊢ (((𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋) ∧ ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
77	43, 71, 76	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
78	77	ex 412	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
79	41, 78	sylbird 260	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
80	37, 79	syld 47	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
81	24, 80	sylbird 260	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
82		df-ne 2934	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ (𝑢 ∩ 𝑣) = ∅)
83	82	ralbii 3084	. . . . . . . . . . . 12 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢 ∩ 𝑣) = ∅)
84		ralnex 3064	. . . . . . . . . . . 12 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢 ∩ 𝑣) = ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
85	83, 84	bitri 275	. . . . . . . . . . 11 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
86	85	ralbii 3084	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
87		ralnex 3064	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
88	86, 87	bitri 275	. . . . . . . . 9 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
89		rexnal 3090	. . . . . . . . 9 ⊢ (∃𝑓 ∈ (Fil‘𝑋) ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ¬ ∀𝑓 ∈ (Fil‘𝑋)∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
90	81, 88, 89	3imtr3g 295	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅ → ¬ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
91	90	con4d 115	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅))
92	91	imp 406	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
93	92	an32s 653	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
94	93	expr 456	. . . 4 ⊢ (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅))
95	94	ralrimivva 3181	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅))
96		simpl 482	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ Top)
97	96, 7	sylib 218	. . . 4 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ (TopOn‘𝑋))
98		hausnei2 23331	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Haus ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)))
99	97, 98	syl 17	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → (𝐽 ∈ Haus ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)))
100	95, 99	mpbird 257	. 2 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ Haus)
101	4, 100	impbii 209	1 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∃*wmo 2538 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 Vcvv 3430 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 𝒫 cpw 4542 {csn 4568 ∪ cuni 4851 ‘cfv 6493 (class class class)co 7361 ficfi 9317 fBascfbas 21335 filGencfg 21336 Topctop 22871 TopOnctopon 22888 neicnei 23075 Hauscha 23286 Filcfil 23823 fLim cflim 23912

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-ov 7364 df-oprab 7365 df-mpo 7366 df-om 7812 df-1o 8399 df-2o 8400 df-en 8888 df-fin 8891 df-fi 9318 df-fbas 21344 df-fg 21345 df-top 22872 df-topon 22889 df-nei 23076 df-haus 23293 df-fil 23824 df-flim 23917

This theorem is referenced by: (None)

W3C validator