Theorem ufileu 23928

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 23913	. . . . 5 ⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
2		ufilmax 23916	. . . . . . . 8 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) → 𝐹 = 𝑓)
3	2	3expa 1118	. . . . . . 7 ⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑓) → 𝐹 = 𝑓)
4	3	eqcomd 2742	. . . . . 6 ⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑓) → 𝑓 = 𝐹)
5	4	ex 412	. . . . 5 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
6	1, 5	sylan2 593	. . . 4 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
7	6	ralrimiva 3145	. . 3 ⊢ (𝐹 ∈ (UFil‘𝑋) → ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
8		ssid 4005	. . . 4 ⊢ 𝐹 ⊆ 𝐹
9		sseq2 4009	. . . . 5 ⊢ (𝑓 = 𝐹 → (𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝐹))
10	9	eqreu 3734	. . . 4 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐹 ⊆ 𝐹 ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
11	8, 10	mp3an2 1450	. . 3 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
12	7, 11	mpdan 687	. 2 ⊢ (𝐹 ∈ (UFil‘𝑋) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
13		reu6 3731	. . 3 ⊢ (∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 ↔ ∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔))
14		ibibr 368	. . . . . . . . . 10 ⊢ ((𝑓 = 𝑔 → 𝐹 ⊆ 𝑓) ↔ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)))
15	14	pm5.74ri 272	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ (𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)))
16		sseq2 4009	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝑔))
17	15, 16	bitr3d 281	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ↔ 𝐹 ⊆ 𝑔))
18	17	rspcva 3619	. . . . . . 7 ⊢ ((𝑔 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ⊆ 𝑔)
19	18	adantll 714	. . . . . 6 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ⊆ 𝑔)
20		ufilfil 23913	. . . . . . . . . 10 ⊢ (𝑔 ∈ (UFil‘𝑋) → 𝑔 ∈ (Fil‘𝑋))
21		filelss 23861	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑔) → 𝑥 ⊆ 𝑋)
22	21	ex 412	. . . . . . . . . 10 ⊢ (𝑔 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
23	20, 22	syl 17	. . . . . . . . 9 ⊢ (𝑔 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
24	23	ad2antlr 727	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
25		filsspw 23860	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
26	25	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ⊆ 𝒫 𝑋)
27		difss 4135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋
28		filtop 23864	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
29	28	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑋 ∈ 𝐹)
30	29	difexd 5330	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ V)
31		elpwg 4602	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∖ 𝑥) ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
33	27, 32	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋)
34	33	snssd 4808	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → {(𝑋 ∖ 𝑥)} ⊆ 𝒫 𝑋)
35	26, 34	unssd 4191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋)
36		ssun1 4177	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)})
37		filn0 23871	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
38	37	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ≠ ∅)
39		ssn0 4403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
40	36, 38, 39	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
41		filelss 23861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑓 ∈ 𝐹) → 𝑓 ⊆ 𝑋)
42	41	ad2ant2rl 749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → 𝑓 ⊆ 𝑋)
43		dfss2 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 ⊆ 𝑋 ↔ (𝑓 ∩ 𝑋) = 𝑓)
44	42, 43	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (𝑓 ∩ 𝑋) = 𝑓)
45	44	sseq1d 4014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → ((𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑥))
46		filss 23862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑓 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑓 ⊆ 𝑥)) → 𝑥 ∈ 𝐹)
47	46	3exp2 1354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑓 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹))))
48	47	impcomd 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))
49	48	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) → ((𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))
50	49	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹))
51	45, 50	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → ((𝑓 ∩ 𝑋) ⊆ 𝑥 → 𝑥 ∈ 𝐹))
52	51	con3d 152	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (¬ 𝑥 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
53	52	expr 456	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥 ⊆ 𝑋) → (𝑓 ∈ 𝐹 → (¬ 𝑥 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)))
54	53	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑓 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)))
55	54	impr 454	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑓 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
56	55	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)
57		ineq2 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 = (𝑋 ∖ 𝑥) → (𝑓 ∩ 𝑔) = (𝑓 ∩ (𝑋 ∖ 𝑥)))
58	57	neeq1d 2999	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 = (𝑋 ∖ 𝑥) → ((𝑓 ∩ 𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
59	58	ralsng 4674	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
60		inssdif0 4373	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) = ∅)
61	60	necon3bbii 2987	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ (𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)
62	59, 61	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
63	30, 62	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
64	63	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
65	56, 64	mpbird 257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅)
66	65	ralrimiva 3145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅)
67		filfbas 23857	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
68	67	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ∈ (fBas‘𝑋))
69		difssd 4136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ⊆ 𝑋)
70		ssdif0 4365	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑋 ⊆ 𝑥 ↔ (𝑋 ∖ 𝑥) = ∅)
71		eqss 3998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑋 ↔ (𝑥 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝑥))
72	71	simplbi2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ⊆ 𝑋 → (𝑋 ⊆ 𝑥 → 𝑥 = 𝑋))
73		eleq1 2828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝐹 ↔ 𝑋 ∈ 𝐹))
74	73	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑋 → (¬ 𝑥 ∈ 𝐹 ↔ ¬ 𝑋 ∈ 𝐹))
75	74	biimpcd 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (¬ 𝑥 ∈ 𝐹 → (𝑥 = 𝑋 → ¬ 𝑋 ∈ 𝐹))
76	72, 75	sylan9 507	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹) → (𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹))
77	76	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹))
78	70, 77	biimtrrid 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋 ∖ 𝑥) = ∅ → ¬ 𝑋 ∈ 𝐹))
79	78	necon2ad 2954	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅))
80	29, 79	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ≠ ∅)
81		snfbas 23875	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅ ∧ 𝑋 ∈ 𝐹) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
82	69, 80, 29, 81	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
83		fbunfip 23878	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅))
84	68, 82, 83	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅))
85	66, 84	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
86		fsubbas 23876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
87	29, 86	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
88	35, 40, 85, 87	mpbir3and 1342	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋))
89		fgcl 23887	. . . . . . . . . . . . . . . . . . 19 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
91		filssufil 23921	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
92	90, 91	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
93		r19.29 3113	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ∃𝑓 ∈ (UFil‘𝑋)((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓))
94		biimp 215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝑔))
95		simpll 766	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ∈ (Fil‘𝑋))
96		snex 5435	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {(𝑋 ∖ 𝑥)} ∈ V
97		unexg 7764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ V) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
98	95, 96, 97	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
99		ssfii 9460	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
100	98, 99	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
101		ssfg 23881	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
102	88, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
103	100, 102	sstrd 3993	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
104	103	unssad 4192	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
105		sstr2 3989	. . . . . . . . . . . . . . . . . . . . . . 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 4009	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ↔ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
109	108	biimpcd 249	. . . . . . . . . . . . . . . . . . . . . 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 410	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
113	112	rexlimdvw 3159	. . . . . . . . . . . . . . . . . 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 406	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)
117	116	an32s 652	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)
118		snidg 4659	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
119	30, 118	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
120		elun2 4182	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)} → (𝑋 ∖ 𝑥) ∈ (𝐹 ∪ {(𝑋 ∖ 𝑥)}))
121	119, 120	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝐹 ∪ {(𝑋 ∖ 𝑥)}))
122	103, 121	sseldd 3983	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
123	122	adantlr 715	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
124	117, 123	sseldd 3983	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ 𝑔)
125		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑔 ∈ (UFil‘𝑋))
126		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑥 ⊆ 𝑋)
127		ufilb 23915	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝑔 ↔ (𝑋 ∖ 𝑥) ∈ 𝑔))
128	125, 126, 127	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (¬ 𝑥 ∈ 𝑔 ↔ (𝑋 ∖ 𝑥) ∈ 𝑔))
129	124, 128	mpbird 257	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ¬ 𝑥 ∈ 𝑔)
130	129	expr 456	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ 𝑔))
131	130	con4d 115	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹))
132	131	ex 412	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹)))
133	132	com23 86	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → (𝑥 ⊆ 𝑋 → 𝑥 ∈ 𝐹)))
134	24, 133	mpdd 43	. . . . . . 7 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹))
135	134	ssrdv 3988	. . . . . 6 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝑔 ⊆ 𝐹)
136	19, 135	eqssd 4000	. . . . 5 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 = 𝑔)
137		simplr 768	. . . . 5 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝑔 ∈ (UFil‘𝑋))
138	136, 137	eqeltrd 2840	. . . 4 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ∈ (UFil‘𝑋))
139	138	rexlimdva2 3156	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → 𝐹 ∈ (UFil‘𝑋)))
140	13, 139	biimtrid 242	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 → 𝐹 ∈ (UFil‘𝑋)))
141	12, 140	impbid2 226	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ (UFil‘𝑋) ↔ ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  ∃!wreu 3377  Vcvv 3479   ∖ cdif 3947   ∪ cun 3948   ∩ cin 3949   ⊆ wss 3950  ∅c0 4332  𝒫 cpw 4599  {csn 4625  ‘cfv 6560  (class class class)co 7432  ficfi 9451  fBascfbas 21353  filGencfg 21354  Filcfil 23854  UFilcufil 23908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-ac2 10504

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-rpss 7744  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-oadd 8511  df-er 8746  df-en 8987  df-dom 8988  df-fin 8990  df-fi 9452  df-dju 9942  df-card 9980  df-ac 10157  df-fbas 21362  df-fg 21363  df-fil 23855  df-ufil 23910

This theorem is referenced by: (None)