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		difexg	$⊢ X \in F \to X ∖ x \in V$
31	29 30	syl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \in V$
32		elpwg	$⊢ X ∖ x \in V \to (X ∖ x \in 𝒫 X \leftrightarrow X ∖ x \subseteq X)$
33	31 32	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)$
34	27 33	mpbiri	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \in 𝒫 X$
35	34	snssd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to \{X ∖ x\} \subseteq 𝒫 X$
36	26 35	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$
37		ssun1	$⊢ F \subseteq F \cup \{X ∖ x\}$
38		filn0	$⊢ F \in Fil (X) \to F \neq \emptyset$
39	38	ad2antrr	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \neq \emptyset$
40		ssn0	$⊢ (F \subseteq F \cup \{X ∖ x\} \land F \neq \emptyset) \to F \cup \{X ∖ x\} \neq \emptyset$
41	37 39 40	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$
42		filelss	$⊢ (F \in Fil (X) \land f \in F) \to f \subseteq X$
43	42	ad2ant2rl	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land f \in F)) \to f \subseteq X$
44		df-ss	$⊢ f \subseteq X \leftrightarrow f \cap X = f$
45	43 44	sylib	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land f \in F)) \to f \cap X = f$
46	45	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)$
47		filss	$⊢ (F \in Fil (X) \land (f \in F \land x \subseteq X \land f \subseteq x)) \to x \in F$
48	47	3exp2	$⊢ F \in Fil (X) \to (f \in F \to (x \subseteq X \to (f \subseteq x \to x \in F)))$
49	48	impcomd	$⊢ F \in Fil (X) \to ((x \subseteq X \land f \in F) \to (f \subseteq x \to x \in F))$
50	49	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))$
51	50	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)$
52	46 51	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)$
53	52	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)$
54	53	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))$
55	54	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))$
56	55	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)$
57	56	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$
58		ineq2	$⊢ g = X ∖ x \to f \cap g = f \cap (X ∖ x)$
59	58	neeq1d	$⊢ g = X ∖ x \to (f \cap g \neq \emptyset \leftrightarrow f \cap (X ∖ x) \neq \emptyset)$
60	59	ralsng	$⊢ X ∖ x \in V \to (\forall g \in \{X ∖ x\} f \cap g \neq \emptyset \leftrightarrow f \cap (X ∖ x) \neq \emptyset)$
61		inssdif0	$⊢ f \cap X \subseteq x \leftrightarrow f \cap (X ∖ x) = \emptyset$
62	61	necon3bbii	$⊢ \neg f \cap X \subseteq x \leftrightarrow f \cap (X ∖ x) \neq \emptyset$
63	60 62	bitr4di	$⊢ X ∖ x \in V \to (\forall g \in \{X ∖ x\} f \cap g \neq \emptyset \leftrightarrow \neg f \cap X \subseteq x)$
64	31 63	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)$
65	64	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)$
66	57 65	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$
67	66	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$
68		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
69	68	ad2antrr	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \in fBas (X)$
70		difssd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \subseteq X$
71		ssdif0	$⊢ X \subseteq x \leftrightarrow X ∖ x = \emptyset$
72		eqss	$⊢ x = X \leftrightarrow (x \subseteq X \land X \subseteq x)$
73	72	simplbi2	$⊢ x \subseteq X \to (X \subseteq x \to x = X)$
74		eleq1	$⊢ x = X \to (x \in F \leftrightarrow X \in F)$
75	74	notbid	$⊢ x = X \to (\neg x \in F \leftrightarrow \neg X \in F)$
76	75	biimpcd	$⊢ \neg x \in F \to (x = X \to \neg X \in F)$
77	73 76	sylan9	$⊢ (x \subseteq X \land \neg x \in F) \to (X \subseteq x \to \neg X \in F)$
78	77	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)$
79	71 78	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)$
80	79	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)$
81	29 80	mpd	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to X ∖ x \neq \emptyset$
82		snfbas	$⊢ (X ∖ x \subseteq X \land X ∖ x \neq \emptyset \land X \in F) \to \{X ∖ x\} \in fBas (X)$
83	70 81 29 82	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)$
84		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)$
85	69 83 84	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)$
86	67 85	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\})$
87		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\})))$
88	29 87	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\})))$
89	36 41 86 88	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)$
90		fgcl	$⊢ fi (F \cup \{X ∖ x\}) \in fBas (X) \to X filGen fi (F \cup \{X ∖ x\}) \in Fil (X)$
91	89 90	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)$
92		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$
93	91 92	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$
94		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)$
95		biimp	$⊢ (F \subseteq f \leftrightarrow f = g) \to (F \subseteq f \to f = g)$
96		simpll	$⊢ ((F \in Fil (X) \land g \in UFil (X)) \land (x \subseteq X \land \neg x \in F)) \to F \in Fil (X)$
97		snex	$⊢ \{X ∖ x\} \in V$
98		unexg	$⊢ (F \in Fil (X) \land \{X ∖ x\} \in V) \to F \cup \{X ∖ x\} \in V$
99	96 97 98	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$
100		ssfii	$⊢ F \cup \{X ∖ x\} \in V \to F \cup \{X ∖ x\} \subseteq fi (F \cup \{X ∖ x\})$
101	99 100	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\})$
102		ssfg	$⊢ fi (F \cup \{X ∖ x\}) \in fBas (X) \to fi (F \cup \{X ∖ x\}) \subseteq X filGen fi (F \cup \{X ∖ x\})$
103	89 102	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\})$
104	101 103	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\})$
105	104	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\})$
106		sstr2	$⊢ F \subseteq X filGen fi (F \cup \{X ∖ x\}) \to (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \to F \subseteq f)$
107	105 106	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)$
108	107	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))$
109		sseq2	$⊢ f = g \to (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \leftrightarrow X filGen fi (F \cup \{X ∖ x\}) \subseteq g)$
110	109	biimpcd	$⊢ X filGen fi (F \cup \{X ∖ x\}) \subseteq f \to (f = g \to X filGen fi (F \cup \{X ∖ x\}) \subseteq g)$
111	110	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)$
112	95 108 111	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))$
113	112	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)$
114	113	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)$
115	94 114	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)$
116	93 115	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)$
117	116	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$
118	117	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$
119		snidg	$⊢ X ∖ x \in V \to X ∖ x \in \{X ∖ x\}$
120	31 119	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\}$
121		elun2	$⊢ X ∖ x \in \{X ∖ x\} \to X ∖ x \in (F \cup \{X ∖ x\})$
122	120 121	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\})$
123	104 122	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\}))$
124	123	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\}))$
125	118 124	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$
126		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)$
127		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$
128		ufilb	$⊢ (g \in UFil (X) \land x \subseteq X) \to (\neg x \in g \leftrightarrow X ∖ x \in g)$
129	126 127 128	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)$
130	125 129	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$
131	130	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)$
132	131	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)$
133	132	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))$
134	133	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))$
135	24 134	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)$
136	135	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$
137	19 136	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$
138		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)$
139	137 138	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)$
140	139	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))$
141	13 140	syl5bi	$⊢ F \in Fil (X) \to (\exists! f \in UFil (X) F \subseteq f \to F \in UFil (X))$
142	12 141	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