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 23964

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 23314	. . 3 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
2		hausflimi 23963	. . . 4 ⊢ (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
3	2	ralrimivw 3135	. . 3 ⊢ (𝐽 ∈ Haus → ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
4	1, 3	jca 516	. 2 ⊢ (𝐽 ∈ Haus → (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
5		flimcf.1	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = ∪ 𝐽
6	5	toptopon 22900	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
7	6	birani 504	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝐽 ∈ (TopOn‘𝑋))
8		simprll 784	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑧 ∈ 𝑋)
9	8	snssd 4718	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑧} ⊆ 𝑋)
10	8	snn0d 4707	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑧} ≠ ∅)
11		neifil 23863	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑧} ⊆ 𝑋 ∧ {𝑧} ≠ ∅) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
12	7, 9, 10, 11	syl3anc 1379	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
13		filfbas 23831	. . . . . . . . . . . 12 ⊢ (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
14	12, 13	syl 17	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
15		simprlr 785	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑤 ∈ 𝑋)
16	15	snssd 4718	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑤} ⊆ 𝑋)
17	15	snn0d 4707	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑤} ≠ ∅)
18		neifil 23863	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑤} ⊆ 𝑋 ∧ {𝑤} ≠ ∅) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
19	7, 16, 17, 18	syl3anc 1379	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
20		filfbas 23831	. . . . . . . . . . . 12 ⊢ (((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
21	19, 20	syl 17	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
22		fbunfip 23852	. . . . . . . . . . 11 ⊢ ((((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋) ∧ ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅))
23	14, 21, 22	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅))
24	5	neisspw 23090	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑧}) ⊆ 𝒫 𝑋)
25	5	neisspw 23090	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑤}) ⊆ 𝒫 𝑋)
26	24, 25	unssd 4121	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋)
27	26	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋)
28	27	a1d 25	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋))
29		ssun1 4107	. . . . . . . . . . . . . 14 ⊢ ((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))
30		filn0 23845	. . . . . . . . . . . . . . 15 ⊢ (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
31	12, 30	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
32		ssn0 4332	. . . . . . . . . . . . . 14 ⊢ ((((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∧ ((nei‘𝐽)‘{𝑧}) ≠ ∅) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅)
33	29, 31, 32	sylancr 593	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅)
34	33	a1d 25	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅))
35		idd 24	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
36	28, 34, 35	3jcad 1135	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
37	5	topopn 22889	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
38	37	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑋 ∈ 𝐽)
39		fsubbas 23850	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝐽 → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
40	38, 39	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
41		fgcl 23861	. . . . . . . . . . . . . . 15 ⊢ ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋))
42	41	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋))
43		simplrr 783	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ≠ 𝑤)
44	8	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ∈ 𝑋)
45	15	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑤 ∈ 𝑋)
46		fvex 6840	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((nei‘𝐽)‘{𝑧}) ∈ V
47		fvex 6840	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((nei‘𝐽)‘{𝑤}) ∈ V
48	46, 47	unex 7687	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V
49		ssfii 9322	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))
50	48, 49	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))
51		ssfg 23855	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
52	51	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
53	50, 52	sstrid 3926	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
54	29, 53	sstrid 3926	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
55	7	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
56		elflim 23954	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
57	55, 42, 56	syl2anc 590	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
58	44, 54, 57	mpbir2and 719	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
59	53	unssbd 4123	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
60		elflim 23954	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
61	55, 42, 60	syl2anc 590	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
62	45, 59, 61	mpbir2and 719	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
63		eleq1w 2822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
64		eleq1w 2822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
65	63, 64	moi 3659	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → 𝑧 = 𝑤)
66	65	3com23 1132	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → 𝑧 = 𝑤)
67	66	3expia 1127	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
68	44, 45, 58, 62, 67	syl22anc 844	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
69	68	necon3ad 2947	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑧 ≠ 𝑤 → ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
70	43, 69	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
71		oveq2 7364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝐽 fLim 𝑓) = (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
72	71	eleq2d 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝑥 ∈ (𝐽 fLim 𝑓) ↔ 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
73	72	mobidv 2553	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ∃𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
74	73	notbid 319	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (¬ ∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
75	74	rspcev 3560	. . . . . . . . . . . . . 14 ⊢ (((𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋) ∧ ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
76	42, 70, 75	syl2anc 590	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
77	76	ex 413	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
78	40, 77	sylbird 261	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
79	36, 78	syld 47	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
80	23, 79	sylbird 261	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
81		df-ne 2935	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ (𝑢 ∩ 𝑣) = ∅)
82	81	ralbii 3085	. . . . . . . . . . . 12 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢 ∩ 𝑣) = ∅)
83		ralnex 3065	. . . . . . . . . . . 12 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢 ∩ 𝑣) = ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
84	82, 83	bitri 276	. . . . . . . . . . 11 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
85	84	ralbii 3085	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
86		ralnex 3065	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
87	85, 86	bitri 276	. . . . . . . . 9 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
88		rexnal 3091	. . . . . . . . 9 ⊢ (∃𝑓 ∈ (Fil‘𝑋) ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ¬ ∀𝑓 ∈ (Fil‘𝑋)∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
89	80, 87, 88	3imtr3g 296	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅ → ¬ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
90	89	con4d 115	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅))
91	90	imp 407	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
92	91	an32s 658	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
93	92	expr 457	. . . 4 ⊢ (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅))
94	93	ralrimivva 3182	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅))
95	6	birani 504	. . . 4 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ (TopOn‘𝑋))
96		hausnei2 23336	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Haus ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)))
97	95, 96	syl 17	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → (𝐽 ∈ Haus ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)))
98	94, 97	mpbird 258	. 2 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ Haus)
99	4, 98	impbii 210	1 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ∃*wmo 2541 ≠ wne 2934 ∀wral 3053 ∃wrex 3063 Vcvv 3431 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4261 𝒫 cpw 4529 {csn 4555 ∪ cuni 4838 ‘cfv 6485 (class class class)co 7356 ficfi 9313 fBascfbas 21335 filGencfg 21336 Topctop 22876 TopOnctopon 22893 neicnei 23080 Hauscha 23291 Filcfil 23828 fLim cflim 23917

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1o 8395 df-2o 8396 df-en 8884 df-fin 8887 df-fi 9314 df-fbas 21344 df-fg 21345 df-top 22877 df-topon 22894 df-nei 23081 df-haus 23298 df-fil 23829 df-flim 23922

This theorem is referenced by: (None)

W3C validator