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 23923

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 23273	. . 3 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
2		hausflimi 23922	. . . 4 ⊢ (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
3	2	ralrimivw 3130	. . 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 22859	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
8	5, 7	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝐽 ∈ (TopOn‘𝑋))
9		simprll 778	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑧 ∈ 𝑋)
10	9	snssd 4763	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑧} ⊆ 𝑋)
11	9	snn0d 4730	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑧} ≠ ∅)
12		neifil 23822	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑧} ⊆ 𝑋 ∧ {𝑧} ≠ ∅) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
13	8, 10, 11, 12	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
14		filfbas 23790	. . . . . . . . . . . 12 ⊢ (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
15	13, 14	syl 17	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
16		simprlr 779	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑤 ∈ 𝑋)
17	16	snssd 4763	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑤} ⊆ 𝑋)
18	16	snn0d 4730	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑤} ≠ ∅)
19		neifil 23822	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑤} ⊆ 𝑋 ∧ {𝑤} ≠ ∅) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
20	8, 17, 18, 19	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
21		filfbas 23790	. . . . . . . . . . . 12 ⊢ (((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
23		fbunfip 23811	. . . . . . . . . . 11 ⊢ ((((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋) ∧ ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅))
24	15, 22, 23	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅))
25	6	neisspw 23049	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑧}) ⊆ 𝒫 𝑋)
26	6	neisspw 23049	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑤}) ⊆ 𝒫 𝑋)
27	25, 26	unssd 4142	. . . . . . . . . . . . . 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 4128	. . . . . . . . . . . . . 14 ⊢ ((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))
31		filn0 23804	. . . . . . . . . . . . . . 15 ⊢ (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
32	13, 31	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
33		ssn0 4354	. . . . . . . . . . . . . 14 ⊢ ((((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∧ ((nei‘𝐽)‘{𝑧}) ≠ ∅) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅)
34	30, 32, 33	sylancr 587	. . . . . . . . . . . . 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 1129	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
38	6	topopn 22848	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
39	38	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑋 ∈ 𝐽)
40		fsubbas 23809	. . . . . . . . . . . . 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 23820	. . . . . . . . . . . . . . 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 777	. . . . . . . . . . . . . . 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 6845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((nei‘𝐽)‘{𝑧}) ∈ V
48		fvex 6845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((nei‘𝐽)‘{𝑤}) ∈ V
49	47, 48	unex 7687	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V
50		ssfii 9320	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))
51	49, 50	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))
52		ssfg 23814	. . . . . . . . . . . . . . . . . . . . 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 3943	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
55	30, 54	sstrid 3943	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
56	8	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
57		elflim 23913	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
58	56, 43, 57	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
59	45, 55, 58	mpbir2and 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
60	54	unssbd 4144	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
61		elflim 23913	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
62	56, 43, 61	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
63	46, 60, 62	mpbir2and 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
64		eleq1w 2817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
65		eleq1w 2817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
66	64, 65	moi 3674	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → 𝑧 = 𝑤)
67	66	3com23 1126	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → 𝑧 = 𝑤)
68	67	3expia 1121	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
69	45, 46, 59, 63, 68	syl22anc 838	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
70	69	necon3ad 2943	. . . . . . . . . . . . . . 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 7364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝐽 fLim 𝑓) = (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
73	72	eleq2d 2820	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝑥 ∈ (𝐽 fLim 𝑓) ↔ 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
74	73	mobidv 2547	. . . . . . . . . . . . . . . 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 3574	. . . . . . . . . . . . . 14 ⊢ (((𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋) ∧ ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
77	43, 71, 76	syl2anc 584	. . . . . . . . . . . . 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 2931	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ (𝑢 ∩ 𝑣) = ∅)
83	82	ralbii 3080	. . . . . . . . . . . 12 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢 ∩ 𝑣) = ∅)
84		ralnex 3060	. . . . . . . . . . . 12 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢 ∩ 𝑣) = ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
85	83, 84	bitri 275	. . . . . . . . . . 11 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
86	85	ralbii 3080	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
87		ralnex 3060	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
88	86, 87	bitri 275	. . . . . . . . 9 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
89		rexnal 3086	. . . . . . . . 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 652	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
94	93	expr 456	. . . 4 ⊢ (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅))
95	94	ralrimivva 3177	. . 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 23295	. . . 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 1086 = wceq 1541 ∈ wcel 2113 ∃*wmo 2535 ≠ wne 2930 ∀wral 3049 ∃wrex 3058 Vcvv 3438 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4283 𝒫 cpw 4552 {csn 4578 ∪ cuni 4861 ‘cfv 6490 (class class class)co 7356 ficfi 9311 fBascfbas 21295 filGencfg 21296 Topctop 22835 TopOnctopon 22852 neicnei 23039 Hauscha 23250 Filcfil 23787 fLim cflim 23876

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1o 8395 df-2o 8396 df-en 8882 df-fin 8885 df-fi 9312 df-fbas 21304 df-fg 21305 df-top 22836 df-topon 22853 df-nei 23040 df-haus 23257 df-fil 23788 df-flim 23881

This theorem is referenced by: (None)

W3C validator