Theorem ufileu 22225

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.)

Assertion

Ref	Expression
ufileu	⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ (UFil‘𝑋) ↔ ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓))

Distinct variable groups:   𝑓,𝐹   𝑓,𝑋

Proof of Theorem ufileu

Dummy variables 𝑔 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ufilfil 22210	. . . . 5 ⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
2		ufilmax 22213	. . . . . . . 8 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) → 𝐹 = 𝑓)
3	2	3expa 1098	. . . . . . 7 ⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑓) → 𝐹 = 𝑓)
4	3	eqcomd 2778	. . . . . 6 ⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑓) → 𝑓 = 𝐹)
5	4	ex 405	. . . . 5 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
6	1, 5	sylan2 583	. . . 4 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
7	6	ralrimiva 3126	. . 3 ⊢ (𝐹 ∈ (UFil‘𝑋) → ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
8		ssid 3873	. . . 4 ⊢ 𝐹 ⊆ 𝐹
9		sseq2 3877	. . . . 5 ⊢ (𝑓 = 𝐹 → (𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝐹))
10	9	eqreu 3626	. . . 4 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐹 ⊆ 𝐹 ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
11	8, 10	mp3an2 1428	. . 3 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
12	7, 11	mpdan 674	. 2 ⊢ (𝐹 ∈ (UFil‘𝑋) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
13		reu6 3623	. . 3 ⊢ (∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 ↔ ∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔))
14		ibibr 361	. . . . . . . . . 10 ⊢ ((𝑓 = 𝑔 → 𝐹 ⊆ 𝑓) ↔ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)))
15	14	pm5.74ri 264	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ (𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)))
16		sseq2 3877	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝑔))
17	15, 16	bitr3d 273	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ↔ 𝐹 ⊆ 𝑔))
18	17	rspcva 3527	. . . . . . 7 ⊢ ((𝑔 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ⊆ 𝑔)
19	18	adantll 701	. . . . . 6 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ⊆ 𝑔)
20		ufilfil 22210	. . . . . . . . . 10 ⊢ (𝑔 ∈ (UFil‘𝑋) → 𝑔 ∈ (Fil‘𝑋))
21		filelss 22158	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑔) → 𝑥 ⊆ 𝑋)
22	21	ex 405	. . . . . . . . . 10 ⊢ (𝑔 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
23	20, 22	syl 17	. . . . . . . . 9 ⊢ (𝑔 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
24	23	ad2antlr 714	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
25		filsspw 22157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
26	25	ad2antrr 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ⊆ 𝒫 𝑋)
27		difss 3992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋
28		filtop 22161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
29	28	ad2antrr 713	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑋 ∈ 𝐹)
30		difexg 5081	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∈ 𝐹 → (𝑋 ∖ 𝑥) ∈ V)
31	29, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ V)
32		elpwg 4424	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∖ 𝑥) ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
33	31, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
34	27, 33	mpbiri 250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋)
35	34	snssd 4610	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → {(𝑋 ∖ 𝑥)} ⊆ 𝒫 𝑋)
36	26, 35	unssd 4044	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋)
37		ssun1 4031	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)})
38		filn0 22168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
39	38	ad2antrr 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ≠ ∅)
40		ssn0 4234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
41	37, 39, 40	sylancr 578	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
42		filelss 22158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑓 ∈ 𝐹) → 𝑓 ⊆ 𝑋)
43	42	ad2ant2rl 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → 𝑓 ⊆ 𝑋)
44		df-ss 3837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 ⊆ 𝑋 ↔ (𝑓 ∩ 𝑋) = 𝑓)
45	43, 44	sylib 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (𝑓 ∩ 𝑋) = 𝑓)
46	45	sseq1d 3882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → ((𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑥))
47		filss 22159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑓 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑓 ⊆ 𝑥)) → 𝑥 ∈ 𝐹)
48	47	3exp2 1334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑓 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹))))
49	48	impcomd 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))
50	49	adantr 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) → ((𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))
51	50	imp 398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹))
52	46, 51	sylbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → ((𝑓 ∩ 𝑋) ⊆ 𝑥 → 𝑥 ∈ 𝐹))
53	52	con3d 150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (¬ 𝑥 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
54	53	expr 449	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥 ⊆ 𝑋) → (𝑓 ∈ 𝐹 → (¬ 𝑥 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)))
55	54	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑓 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)))
56	55	impr 447	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑓 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
57	56	imp 398	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)
58		ineq2 4064	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 = (𝑋 ∖ 𝑥) → (𝑓 ∩ 𝑔) = (𝑓 ∩ (𝑋 ∖ 𝑥)))
59	58	neeq1d 3020	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 = (𝑋 ∖ 𝑥) → ((𝑓 ∩ 𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
60	59	ralsng 4481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
61		inssdif0 4209	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) = ∅)
62	61	necon3bbii 3008	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ (𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)
63	60, 62	syl6bbr 281	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
64	31, 63	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
65	64	adantr 473	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
66	57, 65	mpbird 249	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅)
67	66	ralrimiva 3126	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅)
68		filfbas 22154	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
69	68	ad2antrr 713	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ∈ (fBas‘𝑋))
70		difssd 3993	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ⊆ 𝑋)
71		ssdif0 4203	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑋 ⊆ 𝑥 ↔ (𝑋 ∖ 𝑥) = ∅)
72		eqss 3867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑋 ↔ (𝑥 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝑥))
73	72	simplbi2 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ⊆ 𝑋 → (𝑋 ⊆ 𝑥 → 𝑥 = 𝑋))
74		eleq1 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝐹 ↔ 𝑋 ∈ 𝐹))
75	74	notbid 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑋 → (¬ 𝑥 ∈ 𝐹 ↔ ¬ 𝑋 ∈ 𝐹))
76	75	biimpcd 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (¬ 𝑥 ∈ 𝐹 → (𝑥 = 𝑋 → ¬ 𝑋 ∈ 𝐹))
77	73, 76	sylan9 500	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹) → (𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹))
78	77	adantl 474	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹))
79	71, 78	syl5bir 235	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋 ∖ 𝑥) = ∅ → ¬ 𝑋 ∈ 𝐹))
80	79	necon2ad 2976	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅))
81	29, 80	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ≠ ∅)
82		snfbas 22172	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅ ∧ 𝑋 ∈ 𝐹) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
83	70, 81, 29, 82	syl3anc 1351	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
84		fbunfip 22175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅))
85	69, 83, 84	syl2anc 576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅))
86	67, 85	mpbird 249	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
87		fsubbas 22173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
88	29, 87	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
89	36, 41, 86, 88	mpbir3and 1322	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋))
90		fgcl 22184	. . . . . . . . . . . . . . . . . . 19 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
91	89, 90	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
92		filssufil 22218	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
93	91, 92	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
94		r19.29 3194	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ∃𝑓 ∈ (UFil‘𝑋)((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓))
95		biimp 207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝑔))
96		simpll 754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ∈ (Fil‘𝑋))
97		snex 5182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {(𝑋 ∖ 𝑥)} ∈ V
98		unexg 7283	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ V) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
99	96, 97, 98	sylancl 577	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
100		ssfii 8672	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
101	99, 100	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
102		ssfg 22178	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
103	89, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
104	101, 103	sstrd 3862	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
105	104	unssad 4045	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
106		sstr2 3859	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝐹 ⊆ 𝑓))
107	105, 106	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝐹 ⊆ 𝑓))
108	107	imim1d 82	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝐹 ⊆ 𝑓 → 𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝑓 = 𝑔)))
109		sseq2 3877	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ↔ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
110	109	biimpcd 241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝑓 = 𝑔 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
111	110	a2i 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
112	95, 108, 111	syl56 36	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)))
113	112	impd 402	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
114	113	rexlimdvw 3229	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∃𝑓 ∈ (UFil‘𝑋)((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
115	94, 114	syl5 34	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
116	93, 115	mpan2d 681	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
117	116	imp 398	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)
118	117	an32s 639	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)
119		snidg 4465	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
120	31, 119	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
121		elun2 4036	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)} → (𝑋 ∖ 𝑥) ∈ (𝐹 ∪ {(𝑋 ∖ 𝑥)}))
122	120, 121	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝐹 ∪ {(𝑋 ∖ 𝑥)}))
123	104, 122	sseldd 3853	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
124	123	adantlr 702	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
125	118, 124	sseldd 3853	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ 𝑔)
126		simpllr 763	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑔 ∈ (UFil‘𝑋))
127		simprl 758	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑥 ⊆ 𝑋)
128		ufilb 22212	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝑔 ↔ (𝑋 ∖ 𝑥) ∈ 𝑔))
129	126, 127, 128	syl2anc 576	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (¬ 𝑥 ∈ 𝑔 ↔ (𝑋 ∖ 𝑥) ∈ 𝑔))
130	125, 129	mpbird 249	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ¬ 𝑥 ∈ 𝑔)
131	130	expr 449	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ 𝑔))
132	131	con4d 115	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹))
133	132	ex 405	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹)))
134	133	com23 86	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → (𝑥 ⊆ 𝑋 → 𝑥 ∈ 𝐹)))
135	24, 134	mpdd 43	. . . . . . 7 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹))
136	135	ssrdv 3858	. . . . . 6 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝑔 ⊆ 𝐹)
137	19, 136	eqssd 3869	. . . . 5 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 = 𝑔)
138		simplr 756	. . . . 5 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝑔 ∈ (UFil‘𝑋))
139	137, 138	eqeltrd 2860	. . . 4 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ∈ (UFil‘𝑋))
140	139	rexlimdva2 3226	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → 𝐹 ∈ (UFil‘𝑋)))
141	13, 140	syl5bi 234	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 → 𝐹 ∈ (UFil‘𝑋)))
142	12, 141	impbid2 218	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ (UFil‘𝑋) ↔ ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1068   = wceq 1507   ∈ wcel 2050   ≠ wne 2961  ∀wral 3082  ∃wrex 3083  ∃!wreu 3084  Vcvv 3409   ∖ cdif 3820   ∪ cun 3821   ∩ cin 3822   ⊆ wss 3823  ∅c0 4172  𝒫 cpw 4416  {csn 4435  ‘cfv 6182  (class class class)co 6970  ficfi 8663  fBascfbas 20229  filGencfg 20230  Filcfil 22151  UFilcufil 22205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-ac2 9677

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-pss 3839  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5306  df-eprel 5311  df-po 5320  df-so 5321  df-fr 5360  df-se 5361  df-we 5362  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-rpss 7261  df-om 7391  df-1st 7495  df-2nd 7496  df-wrecs 7744  df-recs 7806  df-rdg 7844  df-1o 7899  df-oadd 7903  df-er 8083  df-en 8301  df-dom 8302  df-fin 8304  df-fi 8664  df-dju 9118  df-card 9156  df-ac 9330  df-fbas 20238  df-fg 20239  df-fil 22152  df-ufil 22207

This theorem is referenced by: (None)