Theorem ufileu 24250

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 24235	. . . . 5 ⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
2		ufilmax 24238	. . . . . . . 8 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) → 𝐹 = 𝑓)
3	2	3expa 1136	. . . . . . 7 ⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑓) → 𝐹 = 𝑓)
4	3	eqcomd 2769	. . . . . 6 ⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑓) → 𝑓 = 𝐹)
5	4	ex 418	. . . . 5 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
6	1, 5	sylan2 605	. . . 4 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
7	6	ralrimiva 3157	. . 3 ⊢ (𝐹 ∈ (UFil‘𝑋) → ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
8		ssid 3934	. . . 4 ⊢ 𝐹 ⊆ 𝐹
9		sseq2 3938	. . . . 5 ⊢ (𝑓 = 𝐹 → (𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝐹))
10	9	eqreu 3689	. . . 4 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐹 ⊆ 𝐹 ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
11	8, 10	mp3an2 1478	. . 3 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
12	7, 11	mpdan 700	. 2 ⊢ (𝐹 ∈ (UFil‘𝑋) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
13		reu6 3686	. . 3 ⊢ (∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 ↔ ∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔))
14		ibibr 371	. . . . . . . . . 10 ⊢ ((𝑓 = 𝑔 → 𝐹 ⊆ 𝑓) ↔ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)))
15	14	pm5.74ri 275	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ (𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)))
16		sseq2 3938	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝑔))
17	15, 16	bitr3d 284	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ↔ 𝐹 ⊆ 𝑔))
18	17	rspcva 3577	. . . . . . 7 ⊢ ((𝑔 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ⊆ 𝑔)
19	18	adantll 727	. . . . . 6 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ⊆ 𝑔)
20		ufilfil 24235	. . . . . . . . . 10 ⊢ (𝑔 ∈ (UFil‘𝑋) → 𝑔 ∈ (Fil‘𝑋))
21		filelss 24183	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑔) → 𝑥 ⊆ 𝑋)
22	21	ex 418	. . . . . . . . . 10 ⊢ (𝑔 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
23	20, 22	syl 18	. . . . . . . . 9 ⊢ (𝑔 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
24	23	ad2antlr 740	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
25		filsspw 24182	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
26	25	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ⊆ 𝒫 𝑋)
27		difss 4074	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋
28		filtop 24186	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
29	28	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑋 ∈ 𝐹)
30	29	difexd 5296	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ V)
31		elpwg 4562	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∖ 𝑥) ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
32	30, 31	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
33	27, 32	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋)
34	33	snssd 4746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → {(𝑋 ∖ 𝑥)} ⊆ 𝒫 𝑋)
35	26, 34	unssd 4192	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋)
36		ssun1 4178	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)})
37		filn0 24193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
38	37	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ≠ ∅)
39		ssn0 4357	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
40	36, 38, 39	sylancr 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
41		filelss 24183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑓 ∈ 𝐹) → 𝑓 ⊆ 𝑋)
42	41	ad2ant2rl 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → 𝑓 ⊆ 𝑋)
43		dfss2 4096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 ⊆ 𝑋 ↔ (𝑓 ∩ 𝑋) = 𝑓)
44	42, 43	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (𝑓 ∩ 𝑋) = 𝑓)
45	44	sseq1d 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → ((𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑥))
46		filss 24184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑓 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑓 ⊆ 𝑥)) → 𝑥 ∈ 𝐹)
47	46	3exp2 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑓 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹))))
48	47	impcomd 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))
49	48	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) → ((𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))
50	49	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹))
51	45, 50	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → ((𝑓 ∩ 𝑋) ⊆ 𝑥 → 𝑥 ∈ 𝐹))
52	51	con3d 153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (¬ 𝑥 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
53	52	expr 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥 ⊆ 𝑋) → (𝑓 ∈ 𝐹 → (¬ 𝑥 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)))
54	53	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑓 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)))
55	54	impr 460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑓 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
56	55	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)
57		ineq2 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 = (𝑋 ∖ 𝑥) → (𝑓 ∩ 𝑔) = (𝑓 ∩ (𝑋 ∖ 𝑥)))
58	57	neeq1d 3017	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 = (𝑋 ∖ 𝑥) → ((𝑓 ∩ 𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
59	58	ralsng 4635	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
60		inssdif0 4324	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) = ∅)
61	60	necon3bbii 3005	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ (𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)
62	59, 61	bitr4di 292	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
63	30, 62	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
64	63	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
65	56, 64	mpbird 260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅)
66	65	ralrimiva 3157	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅)
67		filfbas 24179	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
68	67	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ∈ (fBas‘𝑋))
69		difssd 4075	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ⊆ 𝑋)
70		ssdif0 4316	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑋 ⊆ 𝑥 ↔ (𝑋 ∖ 𝑥) = ∅)
71		eqss 3927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑋 ↔ (𝑥 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝑥))
72	71	simplbi2 506	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ⊆ 𝑋 → (𝑋 ⊆ 𝑥 → 𝑥 = 𝑋))
73		eleq1 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝐹 ↔ 𝑋 ∈ 𝐹))
74	73	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑋 → (¬ 𝑥 ∈ 𝐹 ↔ ¬ 𝑋 ∈ 𝐹))
75	74	biimpcd 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (¬ 𝑥 ∈ 𝐹 → (𝑥 = 𝑋 → ¬ 𝑋 ∈ 𝐹))
76	72, 75	sylan9 517	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹) → (𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹))
77	76	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹))
78	70, 77	biimtrrid 246	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋 ∖ 𝑥) = ∅ → ¬ 𝑋 ∈ 𝐹))
79	78	necon2ad 2973	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅))
80	29, 79	mpd 16	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ≠ ∅)
81		snfbas 24197	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅ ∧ 𝑋 ∈ 𝐹) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
82	69, 80, 29, 81	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
83		fbunfip 24200	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅))
84	68, 82, 83	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅))
85	66, 84	mpbird 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
86		fsubbas 24198	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
87	29, 86	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
88	35, 40, 85, 87	mpbir3and 1361	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋))
89		fgcl 24209	. . . . . . . . . . . . . . . . . . 19 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
90	88, 89	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
91		filssufil 24243	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
92	90, 91	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
93		r19.29 3128	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ∃𝑓 ∈ (UFil‘𝑋)((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓))
94		biimp 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝑔))
95		simpll 779	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ∈ (Fil‘𝑋))
96		snex 5400	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {(𝑋 ∖ 𝑥)} ∈ V
97		unexg 7767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ V) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
98	95, 96, 97	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
99		ssfii 9421	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
100	98, 99	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
101		ssfg 24203	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
102	88, 101	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
103	100, 102	sstrd 3922	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
104	103	unssad 4193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
105		sstr2 3919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝐹 ⊆ 𝑓))
106	104, 105	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝐹 ⊆ 𝑓))
107	106	imim1d 83	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝐹 ⊆ 𝑓 → 𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝑓 = 𝑔)))
108		sseq2 3938	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ↔ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
109	108	biimpcd 252	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝑓 = 𝑔 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
110	109	a2i 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → 𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
111	94, 107, 110	syl56 37	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)))
112	111	impd 416	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
113	112	rexlimdvw 3171	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∃𝑓 ∈ (UFil‘𝑋)((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
114	93, 113	syl5 35	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
115	92, 114	mpan2d 707	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
116	115	imp 412	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)
117	116	an32s 665	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)
118		snidg 4620	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
119	30, 118	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
120		elun2 4183	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)} → (𝑋 ∖ 𝑥) ∈ (𝐹 ∪ {(𝑋 ∖ 𝑥)}))
121	119, 120	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝐹 ∪ {(𝑋 ∖ 𝑥)}))
122	103, 121	sseldd 3913	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
123	122	adantlr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
124	117, 123	sseldd 3913	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ 𝑔)
125		simpllr 788	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑔 ∈ (UFil‘𝑋))
126		simprl 783	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑥 ⊆ 𝑋)
127		ufilb 24237	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝑔 ↔ (𝑋 ∖ 𝑥) ∈ 𝑔))
128	125, 126, 127	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (¬ 𝑥 ∈ 𝑔 ↔ (𝑋 ∖ 𝑥) ∈ 𝑔))
129	124, 128	mpbird 260	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ¬ 𝑥 ∈ 𝑔)
130	129	expr 462	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ 𝑔))
131	130	con4d 116	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹))
132	131	ex 418	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹)))
133	132	com23 87	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → (𝑥 ⊆ 𝑋 → 𝑥 ∈ 𝐹)))
134	24, 133	mpdd 44	. . . . . . 7 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹))
135	134	ssrdv 3918	. . . . . 6 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝑔 ⊆ 𝐹)
136	19, 135	eqssd 3929	. . . . 5 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 = 𝑔)
137		simplr 781	. . . . 5 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝑔 ∈ (UFil‘𝑋))
138	136, 137	eqeltrd 2863	. . . 4 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ∈ (UFil‘𝑋))
139	138	rexlimdva2 3168	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → 𝐹 ∈ (UFil‘𝑋)))
140	13, 139	biimtrid 245	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 → 𝐹 ∈ (UFil‘𝑋)))
141	12, 140	impbid2 229	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ (UFil‘𝑋) ↔ ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2146   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  ∃!wreu 3366  Vcvv 3453   ⊆ wss 3899   ∖ cdif 4047   ∩ cin 4091   ∪ cun 4151  ∅c0 4280  𝒫 cpw 4559  {csn 4587  ‘cfv 6546  (class class class)co 7427  ficfi 9412  fBascfbas 21678  filGencfg 21679  Filcfil 24176  UFilcufil 24230

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5234  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-ac2 10551

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-int 4910  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-se 5608  df-we 5609  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6310  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7384  df-ov 7430  df-oprab 7431  df-mpo 7432  df-rpss 7746  df-om 7885  df-1st 8008  df-2nd 8009  df-frecs 8310  df-wrecs 8341  df-recs 8390  df-rdg 8429  df-1o 8487  df-2o 8488  df-oadd 8491  df-er 8728  df-en 8985  df-dom 8986  df-fin 8988  df-fi 9413  df-dju 9992  df-card 10030  df-ac 10205  df-fbas 21687  df-fg 21688  df-fil 24177  df-ufil 24232

This theorem is used by: (None)