Theorem ufileu 22770

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 22755	. . . . 5 ⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
2		ufilmax 22758	. . . . . . . 8 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) → 𝐹 = 𝑓)
3	2	3expa 1120	. . . . . . 7 ⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑓) → 𝐹 = 𝑓)
4	3	eqcomd 2742	. . . . . 6 ⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑓) → 𝑓 = 𝐹)
5	4	ex 416	. . . . 5 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
6	1, 5	sylan2 596	. . . 4 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
7	6	ralrimiva 3095	. . 3 ⊢ (𝐹 ∈ (UFil‘𝑋) → ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
8		ssid 3909	. . . 4 ⊢ 𝐹 ⊆ 𝐹
9		sseq2 3913	. . . . 5 ⊢ (𝑓 = 𝐹 → (𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝐹))
10	9	eqreu 3631	. . . 4 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐹 ⊆ 𝐹 ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
11	8, 10	mp3an2 1451	. . 3 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
12	7, 11	mpdan 687	. 2 ⊢ (𝐹 ∈ (UFil‘𝑋) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
13		reu6 3628	. . 3 ⊢ (∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 ↔ ∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔))
14		ibibr 372	. . . . . . . . . 10 ⊢ ((𝑓 = 𝑔 → 𝐹 ⊆ 𝑓) ↔ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)))
15	14	pm5.74ri 275	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ (𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)))
16		sseq2 3913	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝑔))
17	15, 16	bitr3d 284	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ↔ 𝐹 ⊆ 𝑔))
18	17	rspcva 3525	. . . . . . 7 ⊢ ((𝑔 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ⊆ 𝑔)
19	18	adantll 714	. . . . . 6 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ⊆ 𝑔)
20		ufilfil 22755	. . . . . . . . . 10 ⊢ (𝑔 ∈ (UFil‘𝑋) → 𝑔 ∈ (Fil‘𝑋))
21		filelss 22703	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑔) → 𝑥 ⊆ 𝑋)
22	21	ex 416	. . . . . . . . . 10 ⊢ (𝑔 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
23	20, 22	syl 17	. . . . . . . . 9 ⊢ (𝑔 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
24	23	ad2antlr 727	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
25		filsspw 22702	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
26	25	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ⊆ 𝒫 𝑋)
27		difss 4032	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋
28		filtop 22706	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
29	28	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑋 ∈ 𝐹)
30	29	difexd 5207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ V)
31		elpwg 4502	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∖ 𝑥) ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
33	27, 32	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋)
34	33	snssd 4708	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → {(𝑋 ∖ 𝑥)} ⊆ 𝒫 𝑋)
35	26, 34	unssd 4086	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋)
36		ssun1 4072	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)})
37		filn0 22713	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
38	37	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ≠ ∅)
39		ssn0 4301	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
40	36, 38, 39	sylancr 590	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
41		filelss 22703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑓 ∈ 𝐹) → 𝑓 ⊆ 𝑋)
42	41	ad2ant2rl 749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → 𝑓 ⊆ 𝑋)
43		df-ss 3870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 ⊆ 𝑋 ↔ (𝑓 ∩ 𝑋) = 𝑓)
44	42, 43	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (𝑓 ∩ 𝑋) = 𝑓)
45	44	sseq1d 3918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → ((𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑥))
46		filss 22704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑓 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑓 ⊆ 𝑥)) → 𝑥 ∈ 𝐹)
47	46	3exp2 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑓 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹))))
48	47	impcomd 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))
49	48	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) → ((𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))
50	49	imp 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹))
51	45, 50	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → ((𝑓 ∩ 𝑋) ⊆ 𝑥 → 𝑥 ∈ 𝐹))
52	51	con3d 155	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (¬ 𝑥 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
53	52	expr 460	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥 ⊆ 𝑋) → (𝑓 ∈ 𝐹 → (¬ 𝑥 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)))
54	53	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑓 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)))
55	54	impr 458	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑓 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
56	55	imp 410	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)
57		ineq2 4107	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 = (𝑋 ∖ 𝑥) → (𝑓 ∩ 𝑔) = (𝑓 ∩ (𝑋 ∖ 𝑥)))
58	57	neeq1d 2991	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 = (𝑋 ∖ 𝑥) → ((𝑓 ∩ 𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
59	58	ralsng 4575	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
60		inssdif0 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) = ∅)
61	60	necon3bbii 2979	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ (𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)
62	59, 61	bitr4di 292	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
63	30, 62	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
64	63	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
65	56, 64	mpbird 260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅)
66	65	ralrimiva 3095	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅)
67		filfbas 22699	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
68	67	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ∈ (fBas‘𝑋))
69		difssd 4033	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ⊆ 𝑋)
70		ssdif0 4264	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑋 ⊆ 𝑥 ↔ (𝑋 ∖ 𝑥) = ∅)
71		eqss 3902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑋 ↔ (𝑥 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝑥))
72	71	simplbi2 504	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ⊆ 𝑋 → (𝑋 ⊆ 𝑥 → 𝑥 = 𝑋))
73		eleq1 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝐹 ↔ 𝑋 ∈ 𝐹))
74	73	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑋 → (¬ 𝑥 ∈ 𝐹 ↔ ¬ 𝑋 ∈ 𝐹))
75	74	biimpcd 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (¬ 𝑥 ∈ 𝐹 → (𝑥 = 𝑋 → ¬ 𝑋 ∈ 𝐹))
76	72, 75	sylan9 511	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹) → (𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹))
77	76	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹))
78	70, 77	syl5bir 246	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋 ∖ 𝑥) = ∅ → ¬ 𝑋 ∈ 𝐹))
79	78	necon2ad 2947	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅))
80	29, 79	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ≠ ∅)
81		snfbas 22717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅ ∧ 𝑋 ∈ 𝐹) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
82	69, 80, 29, 81	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
83		fbunfip 22720	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅))
84	68, 82, 83	syl2anc 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅))
85	66, 84	mpbird 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
86		fsubbas 22718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
87	29, 86	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
88	35, 40, 85, 87	mpbir3and 1344	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋))
89		fgcl 22729	. . . . . . . . . . . . . . . . . . 19 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
91		filssufil 22763	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
92	90, 91	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
93		r19.29 3166	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ∃𝑓 ∈ (UFil‘𝑋)((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓))
94		biimp 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝑔))
95		simpll 767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ∈ (Fil‘𝑋))
96		snex 5309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {(𝑋 ∖ 𝑥)} ∈ V
97		unexg 7512	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ V) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
98	95, 96, 97	sylancl 589	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
99		ssfii 9013	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
100	98, 99	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
101		ssfg 22723	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
102	88, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
103	100, 102	sstrd 3897	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
104	103	unssad 4087	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
105		sstr2 3894	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝐹 ⊆ 𝑓))
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝐹 ⊆ 𝑓))
107	106	imim1d 82	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝐹 ⊆ 𝑓 → 𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝑓 = 𝑔)))
108		sseq2 3913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ↔ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
109	108	biimpcd 252	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝑓 = 𝑔 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
110	109	a2i 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
111	94, 107, 110	syl56 36	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)))
112	111	impd 414	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
113	112	rexlimdvw 3199	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∃𝑓 ∈ (UFil‘𝑋)((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
114	93, 113	syl5 34	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
115	92, 114	mpan2d 694	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
116	115	imp 410	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)
117	116	an32s 652	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)
118		snidg 4561	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
119	30, 118	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
120		elun2 4077	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)} → (𝑋 ∖ 𝑥) ∈ (𝐹 ∪ {(𝑋 ∖ 𝑥)}))
121	119, 120	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝐹 ∪ {(𝑋 ∖ 𝑥)}))
122	103, 121	sseldd 3888	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
123	122	adantlr 715	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
124	117, 123	sseldd 3888	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ 𝑔)
125		simpllr 776	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑔 ∈ (UFil‘𝑋))
126		simprl 771	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑥 ⊆ 𝑋)
127		ufilb 22757	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝑔 ↔ (𝑋 ∖ 𝑥) ∈ 𝑔))
128	125, 126, 127	syl2anc 587	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (¬ 𝑥 ∈ 𝑔 ↔ (𝑋 ∖ 𝑥) ∈ 𝑔))
129	124, 128	mpbird 260	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ¬ 𝑥 ∈ 𝑔)
130	129	expr 460	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ 𝑔))
131	130	con4d 115	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹))
132	131	ex 416	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹)))
133	132	com23 86	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → (𝑥 ⊆ 𝑋 → 𝑥 ∈ 𝐹)))
134	24, 133	mpdd 43	. . . . . . 7 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹))
135	134	ssrdv 3893	. . . . . 6 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝑔 ⊆ 𝐹)
136	19, 135	eqssd 3904	. . . . 5 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 = 𝑔)
137		simplr 769	. . . . 5 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝑔 ∈ (UFil‘𝑋))
138	136, 137	eqeltrd 2831	. . . 4 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ∈ (UFil‘𝑋))
139	138	rexlimdva2 3196	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → 𝐹 ∈ (UFil‘𝑋)))
140	13, 139	syl5bi 245	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 → 𝐹 ∈ (UFil‘𝑋)))
141	12, 140	impbid2 229	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ (UFil‘𝑋) ↔ ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2112   ≠ wne 2932  ∀wral 3051  ∃wrex 3052  ∃!wreu 3053  Vcvv 3398   ∖ cdif 3850   ∪ cun 3851   ∩ cin 3852   ⊆ wss 3853  ∅c0 4223  𝒫 cpw 4499  {csn 4527  ‘cfv 6358  (class class class)co 7191  ficfi 9004  fBascfbas 20305  filGencfg 20306  Filcfil 22696  UFilcufil 22750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-ac2 10042

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-int 4846  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-se 5495  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-isom 6367  df-riota 7148  df-ov 7194  df-oprab 7195  df-mpo 7196  df-rpss 7489  df-om 7623  df-1st 7739  df-2nd 7740  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-1o 8180  df-oadd 8184  df-er 8369  df-en 8605  df-dom 8606  df-fin 8608  df-fi 9005  df-dju 9482  df-card 9520  df-ac 9695  df-fbas 20314  df-fg 20315  df-fil 22697  df-ufil 22752

This theorem is referenced by: (None)