Theorem ufildr

Description: An ultrafilter gives rise to a connected door topology. (Contributed by Jeff Hankins, 6-Dec-2009) (Revised by Stefan O'Rear, 3-Aug-2015)

	Ref	Expression
Hypothesis	ufildr.1	⊢ 𝐽 = ( 𝐹 ∪ { ∅ } )
Assertion	ufildr	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 ∪ ( Clsd ‘ 𝐽 ) ) = 𝒫 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		ufildr.1	⊢ 𝐽 = ( 𝐹 ∪ { ∅ } )
2		elssuni	⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽 )
3		ufilfil	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
4		filunibas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
5	3 4	syl	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
6	1	unieqi	⊢ ∪ 𝐽 = ∪ ( 𝐹 ∪ { ∅ } )
7		uniun	⊢ ∪ ( 𝐹 ∪ { ∅ } ) = ( ∪ 𝐹 ∪ ∪ { ∅ } )
8		0ex	⊢ ∅ ∈ V
9	8	unisn	⊢ ∪ { ∅ } = ∅
10	9	uneq2i	⊢ ( ∪ 𝐹 ∪ ∪ { ∅ } ) = ( ∪ 𝐹 ∪ ∅ )
11		un0	⊢ ( ∪ 𝐹 ∪ ∅ ) = ∪ 𝐹
12	7 10 11	3eqtri	⊢ ∪ ( 𝐹 ∪ { ∅ } ) = ∪ 𝐹
13	6 12	eqtr2i	⊢ ∪ 𝐹 = ∪ 𝐽
14	5 13	eqtr3di	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
15	14	sseq2d	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ⊆ 𝑋 ↔ 𝑥 ⊆ ∪ 𝐽 ) )
16	2 15	imbitrrid	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ 𝑋 ) )
17		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
18	17	cldss	⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ⊆ ∪ 𝐽 )
19	18 15	imbitrrid	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ⊆ 𝑋 ) )
20	16 19	jaod	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥 ⊆ 𝑋 ) )
21		ufilss	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
22		ssun1	⊢ 𝐹 ⊆ ( 𝐹 ∪ { ∅ } )
23	22 1	sseqtrri	⊢ 𝐹 ⊆ 𝐽
24	23	a1i	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → 𝐹 ⊆ 𝐽 )
25	24	sseld	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐹 → 𝑥 ∈ 𝐽 ) )
26	24	sseld	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 → ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 ) )
27		filconn	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∪ { ∅ } ) ∈ Conn )
28		conntop	⊢ ( ( 𝐹 ∪ { ∅ } ) ∈ Conn → ( 𝐹 ∪ { ∅ } ) ∈ Top )
29	3 27 28	3syl	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐹 ∪ { ∅ } ) ∈ Top )
30	1 29	eqeltrid	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐽 ∈ Top )
31	15	biimpa	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → 𝑥 ⊆ ∪ 𝐽 )
32	17	iscld2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽 ) → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) )
33	30 31 32	syl2an2r	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) )
34	14	difeq1d	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) = ( ∪ 𝐽 ∖ 𝑥 ) )
35	34	eleq1d	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 ↔ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) )
36	35	adantr	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 ↔ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) )
37	33 36	bitr4d	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 ) )
38	26 37	sylibrd	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 → 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) )
39	25 38	orim12d	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) → ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) )
40	21 39	mpd	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) )
41	40	ex	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ⊆ 𝑋 → ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) )
42	20 41	impbid	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ↔ 𝑥 ⊆ 𝑋 ) )
43		elun	⊢ ( 𝑥 ∈ ( 𝐽 ∪ ( Clsd ‘ 𝐽 ) ) ↔ ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) )
44		velpw	⊢ ( 𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋 )
45	42 43 44	3bitr4g	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 ∪ ( Clsd ‘ 𝐽 ) ) ↔ 𝑥 ∈ 𝒫 𝑋 ) )
46	45	eqrdv	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 ∪ ( Clsd ‘ 𝐽 ) ) = 𝒫 𝑋 )