ufileu

Description: If the ultrafilter containing a given filter is unique, the filter is an ultrafilter. (Contributed by Jeff Hankins, 3-Dec-2009) (Revised by Mario Carneiro, 2-Oct-2015)

		Ref	Expression
	Assertion	ufileu	$⊢ F \in Fil (X) \to (F \in UFil (X) \leftrightarrow \exists! f \in UFil (X) F \subseteq f)$

Proof

Step	Hyp	Ref	Expression
1		ufilfil	$⊢ f \in UFil (X) \to f \in Fil (X)$
2		ufilmax	$⊢ (F \in UFil (X) \land f \in Fil (X) \land F \subseteq f) \to F = f$
3	2	3expa	$⊢ ((F \in UFil (X) \land f \in Fil (X)) \land F \subseteq f) \to F = f$
4	3	eqcomd	$⊢ ((F \in UFil (X) \land f \in Fil (X)) \land F \subseteq f) \to f = F$
5	4	ex	$⊢ (F \in UFil (X) \land f \in Fil (X)) \to (F \subseteq f \to f = F)$
6	1 5	sylan2	$⊢ (F \in UFil (X) \land f \in UFil (X)) \to (F \subseteq f \to f = F)$
7	6	ralrimiva	$⊢ F \in UFil (X) \to \forall f \in UFil (X) (F \subseteq f \to f = F)$
8		ssid	$⊢ F \subseteq F$
9		sseq2	$⊢ f = F \to (F \subseteq f \leftrightarrow F \subseteq F)$
10	9	eqreu	$⊢ (F \in UFil (X) \land F \subseteq F \land \forall f \in UFil (X) (F \subseteq f \to f = F)) \to \exists! f \in UFil (X) F \subseteq f$
11	8 10	mp3an2	$⊢ (F \in UFil (X) \land \forall f \in UFil (X) (F \subseteq f \to f = F)) \to \exists! f \in UFil (X) F \subseteq f$
12	7 11	mpdan	$⊢ F \in UFil (X) \to \exists! f \in UFil (X) F \subseteq f$
13		reu6	$⊢ \exists! f \in UFil (X) F \subseteq f \leftrightarrow \exists g \in UFil (X) \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)$
14		ibibr	$⊢ (f = g \to F \subseteq f) \leftrightarrow (f = g \to (F \subseteq f \leftrightarrow f = g))$
15	14	pm5.74ri	$⊢ f = g \to (F \subseteq f \leftrightarrow (F \subseteq f \leftrightarrow f = g))$
16		sseq2	$⊢ f = g \to (F \subseteq f \leftrightarrow F \subseteq g)$
17	15 16	bitr3d	$⊢ f = g \to ((F \subseteq f \leftrightarrow f = g) \leftrightarrow F \subseteq g)$
18	17	rspcva	$⊢ (g \in UFil (X) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \to F \subseteq g$
19	18	adantll	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \to F \subseteq g$
20		ufilfil	$⊢ g \in UFil (X) \to g \in Fil (X)$
21		filelss	$⊢ (g \in Fil (X) \land x \in g) \to x \subseteq X$
22	21	ex	$⊢ g \in Fil (X) \to (x \in g \to x \subseteq X)$
23	20 22	syl	$⊢ g \in UFil (X) \to (x \in g \to x \subseteq X)$
24	23	ad2antlr	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \to (x \in g \to x \subseteq X)$
25		filsspw	$⊢ F \in Fil (X) \to F \subseteq 𝒫 X$
26	25	ad2antrr	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \subseteq 𝒫 X$
27		difss	$⊢ X ∖ x \subseteq X$
28		filtop	$⊢ F \in Fil (X) \to X \in F$
29	28	ad2antrr	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X \in F$
30	29	difexd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \in V$
31		elpwg	$⊢ X ∖ x \in V \to (X ∖ x \in 𝒫 X \leftrightarrow X ∖ x \subseteq X)$
32	30 31	syl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (X ∖ x \in 𝒫 X \leftrightarrow X ∖ x \subseteq X)$
33	27 32	mpbiri	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \in 𝒫 X$
34	33	snssd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to \{X ∖ x\} \subseteq 𝒫 X$
35	26 34	unssd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \cup \{X ∖ x\} \subseteq 𝒫 X$
36		ssun1	$⊢ F \subseteq F \cup \{X ∖ x\}$
37		filn0	$⊢ F \in Fil (X) \to F \neq \emptyset$
38	37	ad2antrr	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \neq \emptyset$
39		ssn0	$⊢ (F \subseteq F \cup \{X ∖ x\} \land F \neq \emptyset) \to F \cup \{X ∖ x\} \neq \emptyset$
40	36 38 39	sylancr	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \cup \{X ∖ x\} \neq \emptyset$
41		filelss	$⊢ (F \in Fil (X) \land f \in F) \to f \subseteq X$
42	41	ad2ant2rl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land f \in F)) \to f \subseteq X$
43		df-ss	$⊢ f \subseteq X \leftrightarrow f \cap X = f$
44	42 43	sylib	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land f \in F)) \to f \cap X = f$
45	44	sseq1d	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land f \in F)) \to (f \cap X \subseteq x \leftrightarrow f \subseteq x)$
46		filss	$⊢ (F \in Fil (X) \land (f \in F \land x \subseteq X \land f \subseteq x)) \to x \in F$
47	46	3exp2	$⊢ F \in Fil (X) \to (f \in F \to (x \subseteq X \to (f \subseteq x \to x \in F)))$
48	47	impcomd	$⊢ F \in Fil (X) \to ((x \subseteq X \land f \in F) \to (f \subseteq x \to x \in F))$
49	48	adantr	$⊢ (F \in Fil (X) \land g \in UFil (X)) \to ((x \subseteq X \land f \in F) \to (f \subseteq x \to x \in F))$
50	49	imp	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land f \in F)) \to (f \subseteq x \to x \in F)$
51	45 50	sylbid	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land f \in F)) \to (f \cap X \subseteq x \to x \in F)$
52	51	con3d	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land f \in F)) \to (\neg x \in F \to \neg f \cap X \subseteq x)$
53	52	expr	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land x \subseteq X) \to (f \in F \to (\neg x \in F \to \neg f \cap X \subseteq x))$
54	53	com23	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land x \subseteq X) \to (\neg x \in F \to (f \in F \to \neg f \cap X \subseteq x))$
55	54	impr	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (f \in F \to \neg f \cap X \subseteq x)$
56	55	imp	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \land f \in F) \to \neg f \cap X \subseteq x$
57		ineq2	$⊢ g = X ∖ x \to f \cap g = f \cap (X ∖ x)$
58	57	neeq1d	$⊢ g = X ∖ x \to (f \cap g \neq \emptyset \leftrightarrow f \cap (X ∖ x) \neq \emptyset)$
59	58	ralsng	$⊢ X ∖ x \in V \to (\forall g \in \{X ∖ x\} f \cap g \neq \emptyset \leftrightarrow f \cap (X ∖ x) \neq \emptyset)$
60		inssdif0	$⊢ f \cap X \subseteq x \leftrightarrow f \cap (X ∖ x) = \emptyset$
61	60	necon3bbii	$⊢ \neg f \cap X \subseteq x \leftrightarrow f \cap (X ∖ x) \neq \emptyset$
62	59 61	bitr4di	$⊢ X ∖ x \in V \to (\forall g \in \{X ∖ x\} f \cap g \neq \emptyset \leftrightarrow \neg f \cap X \subseteq x)$
63	30 62	syl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (\forall g \in \{X ∖ x\} f \cap g \neq \emptyset \leftrightarrow \neg f \cap X \subseteq x)$
64	63	adantr	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \land f \in F) \to (\forall g \in \{X ∖ x\} f \cap g \neq \emptyset \leftrightarrow \neg f \cap X \subseteq x)$
65	56 64	mpbird	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \land f \in F) \to \forall g \in \{X ∖ x\} f \cap g \neq \emptyset$
66	65	ralrimiva	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to \forall f \in F \forall g \in \{X ∖ x\} f \cap g \neq \emptyset$
67		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
68	67	ad2antrr	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \in fBas (X)$
69		difssd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \subseteq X$
70		ssdif0	$⊢ X \subseteq x \leftrightarrow X ∖ x = \emptyset$
71		eqss	$⊢ x = X \leftrightarrow (x \subseteq X \land X \subseteq x)$
72	71	simplbi2	$⊢ x \subseteq X \to (X \subseteq x \to x = X)$
73		eleq1	$⊢ x = X \to (x \in F \leftrightarrow X \in F)$
74	73	notbid	$⊢ x = X \to (\neg x \in F \leftrightarrow \neg X \in F)$
75	74	biimpcd	$⊢ \neg x \in F \to (x = X \to \neg X \in F)$
76	72 75	sylan9	$⊢ (x \subseteq X \land \neg x \in F) \to (X \subseteq x \to \neg X \in F)$
77	76	adantl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (X \subseteq x \to \neg X \in F)$
78	70 77	syl5bir	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (X ∖ x = \emptyset \to \neg X \in F)$
79	78	necon2ad	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (X \in F \to X ∖ x \neq \emptyset)$
80	29 79	mpd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \neq \emptyset$
81		snfbas	$⊢ (X ∖ x \subseteq X \land X ∖ x \neq \emptyset \land X \in F) \to \{X ∖ x\} \in fBas (X)$
82	69 80 29 81	syl3anc	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to \{X ∖ x\} \in fBas (X)$
83		fbunfip	$⊢ (F \in fBas (X) \land \{X ∖ x\} \in fBas (X)) \to (\neg \emptyset \in fi (F \cup \{X ∖ x\}) \leftrightarrow \forall f \in F \forall g \in \{X ∖ x\} f \cap g \neq \emptyset)$
84	68 82 83	syl2anc	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (\neg \emptyset \in fi (F \cup \{X ∖ x\}) \leftrightarrow \forall f \in F \forall g \in \{X ∖ x\} f \cap g \neq \emptyset)$
85	66 84	mpbird	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to \neg \emptyset \in fi (F \cup \{X ∖ x\})$
86		fsubbas	$⊢ X \in F \to (fi (F \cup \{X ∖ x\}) \in fBas (X) \leftrightarrow (F \cup \{X ∖ x\} \subseteq 𝒫 X \land F \cup \{X ∖ x\} \neq \emptyset \land \neg \emptyset \in fi (F \cup \{X ∖ x\})))$
87	29 86	syl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (fi (F \cup \{X ∖ x\}) \in fBas (X) \leftrightarrow (F \cup \{X ∖ x\} \subseteq 𝒫 X \land F \cup \{X ∖ x\} \neq \emptyset \land \neg \emptyset \in fi (F \cup \{X ∖ x\})))$
88	35 40 85 87	mpbir3and	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to fi (F \cup \{X ∖ x\}) \in fBas (X)$
89		fgcl	$⊢ fi (F \cup \{X ∖ x\}) \in fBas (X) \to X filGen fi (F \cup \{X ∖ x\}) \in Fil (X)$
90	88 89	syl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X filGen fi (F \cup \{X ∖ x\}) \in Fil (X)$
91		filssufil	$⊢ X filGen fi (F \cup \{X ∖ x\}) \in Fil (X) \to \exists f \in UFil (X) X filGen fi (F \cup \{X ∖ x\}) \subseteq f$
92	90 91	syl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to \exists f \in UFil (X) X filGen fi (F \cup \{X ∖ x\}) \subseteq f$
93		r19.29	$⊢ (\forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g) \land \exists f \in UFil (X) X filGen fi (F \cup \{X ∖ x\}) \subseteq f) \to \exists f \in UFil (X) ((F \subseteq f \leftrightarrow f = g) \land X filGen fi (F \cup \{X ∖ x\}) \subseteq f)$
94		biimp	$⊢ (F \subseteq f \leftrightarrow f = g) \to (F \subseteq f \to f = g)$
95		simpll	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \in Fil (X)$
96		snex	$⊢ \{X ∖ x\} \in V$
97		unexg	$⊢ (F \in Fil (X) \land \{X ∖ x\} \in V) \to F \cup \{X ∖ x\} \in V$
98	95 96 97	sylancl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \cup \{X ∖ x\} \in V$
99		ssfii	$⊢ F \cup \{X ∖ x\} \in V \to F \cup \{X ∖ x\} \subseteq fi (F \cup \{X ∖ x\})$
100	98 99	syl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \cup \{X ∖ x\} \subseteq fi (F \cup \{X ∖ x\})$
101		ssfg	$⊢ fi (F \cup \{X ∖ x\}) \in fBas (X) \to fi (F \cup \{X ∖ x\}) \subseteq X filGen fi (F \cup \{X ∖ x\})$
102	88 101	syl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to fi (F \cup \{X ∖ x\}) \subseteq X filGen fi (F \cup \{X ∖ x\})$
103	100 102	sstrd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \cup \{X ∖ x\} \subseteq X filGen fi (F \cup \{X ∖ x\})$
104	103	unssad	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \subseteq X filGen fi (F \cup \{X ∖ x\})$
105		sstr2	$⊢ F \subseteq X filGen fi (F \cup \{X ∖ x\}) \to (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \to F \subseteq f)$
106	104 105	syl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \to F \subseteq f)$
107	106	imim1d	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to ((F \subseteq f \to f = g) \to (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \to f = g))$
108		sseq2	$⊢ f = g \to (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \leftrightarrow X filGen fi (F \cup \{X ∖ x\}) \subseteq g)$
109	108	biimpcd	$⊢ X filGen fi (F \cup \{X ∖ x\}) \subseteq f \to (f = g \to X filGen fi (F \cup \{X ∖ x\}) \subseteq g)$
110	109	a2i	$⊢ (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \to f = g) \to (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \to X filGen fi (F \cup \{X ∖ x\}) \subseteq g)$
111	94 107 110	syl56	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to ((F \subseteq f \leftrightarrow f = g) \to (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \to X filGen fi (F \cup \{X ∖ x\}) \subseteq g))$
112	111	impd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (((F \subseteq f \leftrightarrow f = g) \land X filGen fi (F \cup \{X ∖ x\}) \subseteq f) \to X filGen fi (F \cup \{X ∖ x\}) \subseteq g)$
113	112	rexlimdvw	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (\exists f \in UFil (X) ((F \subseteq f \leftrightarrow f = g) \land X filGen fi (F \cup \{X ∖ x\}) \subseteq f) \to X filGen fi (F \cup \{X ∖ x\}) \subseteq g)$
114	93 113	syl5	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to ((\forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g) \land \exists f \in UFil (X) X filGen fi (F \cup \{X ∖ x\}) \subseteq f) \to X filGen fi (F \cup \{X ∖ x\}) \subseteq g)$
115	92 114	mpan2d	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to (\forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g) \to X filGen fi (F \cup \{X ∖ x\}) \subseteq g)$
116	115	imp	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \to X filGen fi (F \cup \{X ∖ x\}) \subseteq g$
117	116	an32s	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \land (x \subseteq X \land \neg x \in F)) \to X filGen fi (F \cup \{X ∖ x\}) \subseteq g$
118		snidg	$⊢ X ∖ x \in V \to X ∖ x \in \{X ∖ x\}$
119	30 118	syl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \in \{X ∖ x\}$
120		elun2	$⊢ X ∖ x \in \{X ∖ x\} \to X ∖ x \in (F \cup \{X ∖ x\})$
121	119 120	syl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \in (F \cup \{X ∖ x\})$
122	103 121	sseldd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \in (X filGen fi (F \cup \{X ∖ x\}))$
123	122	adantlr	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \in (X filGen fi (F \cup \{X ∖ x\}))$
124	117 123	sseldd	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \in g$
125		simpllr	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \land (x \subseteq X \land \neg x \in F)) \to g \in UFil (X)$
126		simprl	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \land (x \subseteq X \land \neg x \in F)) \to x \subseteq X$
127		ufilb	$⊢ (g \in UFil (X) \land x \subseteq X) \to (\neg x \in g \leftrightarrow X ∖ x \in g)$
128	125 126 127	syl2anc	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \land (x \subseteq X \land \neg x \in F)) \to (\neg x \in g \leftrightarrow X ∖ x \in g)$
129	124 128	mpbird	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \land (x \subseteq X \land \neg x \in F)) \to \neg x \in g$
130	129	expr	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \land x \subseteq X) \to (\neg x \in F \to \neg x \in g)$
131	130	con4d	$⊢ (((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \land x \subseteq X) \to (x \in g \to x \in F)$
132	131	ex	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \to (x \subseteq X \to (x \in g \to x \in F))$
133	132	com23	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \to (x \in g \to (x \subseteq X \to x \in F))$
134	24 133	mpdd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \to (x \in g \to x \in F)$
135	134	ssrdv	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \to g \subseteq F$
136	19 135	eqssd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \to F = g$
137		simplr	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \to g \in UFil (X)$
138	136 137	eqeltrd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g)) \to F \in UFil (X)$
139	138	rexlimdva2	$⊢ F \in Fil (X) \to (\exists g \in UFil (X) \forall f \in UFil (X) (F \subseteq f \leftrightarrow f = g) \to F \in UFil (X))$
140	13 139	syl5bi	$⊢ F \in Fil (X) \to (\exists! f \in UFil (X) F \subseteq f \to F \in UFil (X))$
141	12 140	impbid2	$⊢ F \in Fil (X) \to (F \in UFil (X) \leftrightarrow \exists! f \in UFil (X) F \subseteq f)$

Metamath Proof Explorer

Theorem ufileu

Proof