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	$⊢ J = F \cup \{\emptyset\}$
	Assertion	ufildr	$⊢ F \in UFil (X) \to J \cup Clsd (J) = 𝒫 X$

Proof

Step	Hyp	Ref	Expression
1		ufildr.1	$⊢ J = F \cup \{\emptyset\}$
2		elssuni	$⊢ x \in J \to x \subseteq ⋃ J$
3	1	unieqi	$⊢ ⋃ J = ⋃ (F \cup \{\emptyset\})$
4		uniun	$⊢ ⋃ (F \cup \{\emptyset\}) = ⋃ F \cup ⋃ \{\emptyset\}$
5		0ex	$⊢ \emptyset \in V$
6	5	unisn	$⊢ ⋃ \{\emptyset\} = \emptyset$
7	6	uneq2i	$⊢ ⋃ F \cup ⋃ \{\emptyset\} = ⋃ F \cup \emptyset$
8		un0	$⊢ ⋃ F \cup \emptyset = ⋃ F$
9	4 7 8	3eqtri	$⊢ ⋃ (F \cup \{\emptyset\}) = ⋃ F$
10	3 9	eqtr2i	$⊢ ⋃ F = ⋃ J$
11		ufilfil	$⊢ F \in UFil (X) \to F \in Fil (X)$
12		filunibas	$⊢ F \in Fil (X) \to ⋃ F = X$
13	11 12	syl	$⊢ F \in UFil (X) \to ⋃ F = X$
14	10 13	syl5reqr	$⊢ F \in UFil (X) \to X = ⋃ J$
15	14	sseq2d	$⊢ F \in UFil (X) \to (x \subseteq X \leftrightarrow x \subseteq ⋃ J)$
16	2 15	syl5ibr	$⊢ F \in UFil (X) \to (x \in J \to x \subseteq X)$
17		eqid	$⊢ ⋃ J = ⋃ J$
18	17	cldss	$⊢ x \in Clsd (J) \to x \subseteq ⋃ J$
19	18 15	syl5ibr	$⊢ F \in UFil (X) \to (x \in Clsd (J) \to x \subseteq X)$
20	16 19	jaod	$⊢ F \in UFil (X) \to ((x \in J \lor x \in Clsd (J)) \to x \subseteq X)$
21		ufilss	$⊢ (F \in UFil (X) \land x \subseteq X) \to (x \in F \lor X ∖ x \in F)$
22		ssun1	$⊢ F \subseteq F \cup \{\emptyset\}$
23	22 1	sseqtrri	$⊢ F \subseteq J$
24	23	a1i	$⊢ (F \in UFil (X) \land x \subseteq X) \to F \subseteq J$
25	24	sseld	$⊢ (F \in UFil (X) \land x \subseteq X) \to (x \in F \to x \in J)$
26	24	sseld	$⊢ (F \in UFil (X) \land x \subseteq X) \to (X ∖ x \in F \to X ∖ x \in J)$
27		filconn	$⊢ F \in Fil (X) \to F \cup \{\emptyset\} \in Conn$
28		conntop	$⊢ F \cup \{\emptyset\} \in Conn \to F \cup \{\emptyset\} \in Top$
29	11 27 28	3syl	$⊢ F \in UFil (X) \to F \cup \{\emptyset\} \in Top$
30	1 29	eqeltrid	$⊢ F \in UFil (X) \to J \in Top$
31	15	biimpa	$⊢ (F \in UFil (X) \land x \subseteq X) \to x \subseteq ⋃ J$
32	17	iscld2	$⊢ (J \in Top \land x \subseteq ⋃ J) \to (x \in Clsd (J) \leftrightarrow ⋃ J ∖ x \in J)$
33	30 31 32	syl2an2r	$⊢ (F \in UFil (X) \land x \subseteq X) \to (x \in Clsd (J) \leftrightarrow ⋃ J ∖ x \in J)$
34	14	difeq1d	$⊢ F \in UFil (X) \to X ∖ x = ⋃ J ∖ x$
35	34	eleq1d	$⊢ F \in UFil (X) \to (X ∖ x \in J \leftrightarrow ⋃ J ∖ x \in J)$
36	35	adantr	$⊢ (F \in UFil (X) \land x \subseteq X) \to (X ∖ x \in J \leftrightarrow ⋃ J ∖ x \in J)$
37	33 36	bitr4d	$⊢ (F \in UFil (X) \land x \subseteq X) \to (x \in Clsd (J) \leftrightarrow X ∖ x \in J)$
38	26 37	sylibrd	$⊢ (F \in UFil (X) \land x \subseteq X) \to (X ∖ x \in F \to x \in Clsd (J))$
39	25 38	orim12d	$⊢ (F \in UFil (X) \land x \subseteq X) \to ((x \in F \lor X ∖ x \in F) \to (x \in J \lor x \in Clsd (J)))$
40	21 39	mpd	$⊢ (F \in UFil (X) \land x \subseteq X) \to (x \in J \lor x \in Clsd (J))$
41	40	ex	$⊢ F \in UFil (X) \to (x \subseteq X \to (x \in J \lor x \in Clsd (J)))$
42	20 41	impbid	$⊢ F \in UFil (X) \to ((x \in J \lor x \in Clsd (J)) \leftrightarrow x \subseteq X)$
43		elun	$⊢ x \in (J \cup Clsd (J)) \leftrightarrow (x \in J \lor x \in Clsd (J))$
44		velpw	$⊢ x \in 𝒫 X \leftrightarrow x \subseteq X$
45	42 43 44	3bitr4g	$⊢ F \in UFil (X) \to (x \in (J \cup Clsd (J)) \leftrightarrow x \in 𝒫 X)$
46	45	eqrdv	$⊢ F \in UFil (X) \to J \cup Clsd (J) = 𝒫 X$

Metamath Proof Explorer

Theorem ufildr

Proof