Theorem ufileu 23168

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 23153	. . . . 5 ⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
2		ufilmax 23156	. . . . . . . 8 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) → 𝐹 = 𝑓)
3	2	3expa 1117	. . . . . . 7 ⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑓) → 𝐹 = 𝑓)
4	3	eqcomd 2742	. . . . . 6 ⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) ∧ 𝐹 ⊆ 𝑓) → 𝑓 = 𝐹)
5	4	ex 413	. . . . 5 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
6	1, 5	sylan2 593	. . . 4 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
7	6	ralrimiva 3139	. . 3 ⊢ (𝐹 ∈ (UFil‘𝑋) → ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹))
8		ssid 3953	. . . 4 ⊢ 𝐹 ⊆ 𝐹
9		sseq2 3957	. . . . 5 ⊢ (𝑓 = 𝐹 → (𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝐹))
10	9	eqreu 3674	. . . 4 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐹 ⊆ 𝐹 ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
11	8, 10	mp3an2 1448	. . 3 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑓 = 𝐹)) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
12	7, 11	mpdan 684	. 2 ⊢ (𝐹 ∈ (UFil‘𝑋) → ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
13		reu6 3671	. . 3 ⊢ (∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 ↔ ∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔))
14		ibibr 368	. . . . . . . . . 10 ⊢ ((𝑓 = 𝑔 → 𝐹 ⊆ 𝑓) ↔ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)))
15	14	pm5.74ri 271	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ (𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)))
16		sseq2 3957	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝑔))
17	15, 16	bitr3d 280	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ↔ 𝐹 ⊆ 𝑔))
18	17	rspcva 3568	. . . . . . 7 ⊢ ((𝑔 ∈ (UFil‘𝑋) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ⊆ 𝑔)
19	18	adantll 711	. . . . . 6 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ⊆ 𝑔)
20		ufilfil 23153	. . . . . . . . . 10 ⊢ (𝑔 ∈ (UFil‘𝑋) → 𝑔 ∈ (Fil‘𝑋))
21		filelss 23101	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑔) → 𝑥 ⊆ 𝑋)
22	21	ex 413	. . . . . . . . . 10 ⊢ (𝑔 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
23	20, 22	syl 17	. . . . . . . . 9 ⊢ (𝑔 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
24	23	ad2antlr 724	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋))
25		filsspw 23100	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
26	25	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ⊆ 𝒫 𝑋)
27		difss 4077	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋
28		filtop 23104	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
29	28	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑋 ∈ 𝐹)
30	29	difexd 5270	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ V)
31		elpwg 4549	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∖ 𝑥) ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
33	27, 32	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋)
34	33	snssd 4755	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → {(𝑋 ∖ 𝑥)} ⊆ 𝒫 𝑋)
35	26, 34	unssd 4132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋)
36		ssun1 4118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)})
37		filn0 23111	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
38	37	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ≠ ∅)
39		ssn0 4346	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
40	36, 38, 39	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
41		filelss 23101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑓 ∈ 𝐹) → 𝑓 ⊆ 𝑋)
42	41	ad2ant2rl 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → 𝑓 ⊆ 𝑋)
43		df-ss 3914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 ⊆ 𝑋 ↔ (𝑓 ∩ 𝑋) = 𝑓)
44	42, 43	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (𝑓 ∩ 𝑋) = 𝑓)
45	44	sseq1d 3962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → ((𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑥))
46		filss 23102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑓 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑓 ⊆ 𝑥)) → 𝑥 ∈ 𝐹)
47	46	3exp2 1353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑓 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹))))
48	47	impcomd 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))
49	48	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) → ((𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))
50	49	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹))
51	45, 50	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → ((𝑓 ∩ 𝑋) ⊆ 𝑥 → 𝑥 ∈ 𝐹))
52	51	con3d 152	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹)) → (¬ 𝑥 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
53	52	expr 457	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥 ⊆ 𝑋) → (𝑓 ∈ 𝐹 → (¬ 𝑥 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)))
54	53	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑓 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)))
55	54	impr 455	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑓 ∈ 𝐹 → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
56	55	imp 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥)
57		ineq2 4152	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 = (𝑋 ∖ 𝑥) → (𝑓 ∩ 𝑔) = (𝑓 ∩ (𝑋 ∖ 𝑥)))
58	57	neeq1d 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 = (𝑋 ∖ 𝑥) → ((𝑓 ∩ 𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
59	58	ralsng 4620	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
60		inssdif0 4315	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) = ∅)
61	60	necon3bbii 2988	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ (𝑓 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑓 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)
62	59, 61	bitr4di 288	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
63	30, 62	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
64	63	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → (∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅ ↔ ¬ (𝑓 ∩ 𝑋) ⊆ 𝑥))
65	56, 64	mpbird 256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ 𝑓 ∈ 𝐹) → ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅)
66	65	ralrimiva 3139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅)
67		filfbas 23097	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
68	67	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ∈ (fBas‘𝑋))
69		difssd 4078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ⊆ 𝑋)
70		ssdif0 4309	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑋 ⊆ 𝑥 ↔ (𝑋 ∖ 𝑥) = ∅)
71		eqss 3946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑋 ↔ (𝑥 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝑥))
72	71	simplbi2 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ⊆ 𝑋 → (𝑋 ⊆ 𝑥 → 𝑥 = 𝑋))
73		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝐹 ↔ 𝑋 ∈ 𝐹))
74	73	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑋 → (¬ 𝑥 ∈ 𝐹 ↔ ¬ 𝑋 ∈ 𝐹))
75	74	biimpcd 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (¬ 𝑥 ∈ 𝐹 → (𝑥 = 𝑋 → ¬ 𝑋 ∈ 𝐹))
76	72, 75	sylan9 508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹) → (𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹))
77	76	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹))
78	70, 77	syl5bir 242	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((𝑋 ∖ 𝑥) = ∅ → ¬ 𝑋 ∈ 𝐹))
79	78	necon2ad 2955	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅))
80	29, 79	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ≠ ∅)
81		snfbas 23115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅ ∧ 𝑋 ∈ 𝐹) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
82	69, 80, 29, 81	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
83		fbunfip 23118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅))
84	68, 82, 83	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ {(𝑋 ∖ 𝑥)} (𝑓 ∩ 𝑔) ≠ ∅))
85	66, 84	mpbird 256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
86		fsubbas 23116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
87	29, 86	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
88	35, 40, 85, 87	mpbir3and 1341	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋))
89		fgcl 23127	. . . . . . . . . . . . . . . . . . 19 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
91		filssufil 23161	. . . . . . . . . . . . . . . . . 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 214	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → (𝐹 ⊆ 𝑓 → 𝑓 = 𝑔))
95		simpll 764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ∈ (Fil‘𝑋))
96		snex 5373	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {(𝑋 ∖ 𝑥)} ∈ V
97		unexg 7653	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ V) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
98	95, 96, 97	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
99		ssfii 9268	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
100	98, 99	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
101		ssfg 23121	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
102	88, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
103	100, 102	sstrd 3941	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
104	103	unssad 4133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
105		sstr2 3938	. . . . . . . . . . . . . . . . . . . . . . 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 3957	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ↔ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
109	108	biimpcd 248	. . . . . . . . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (((𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
113	112	rexlimdvw 3153	. . . . . . . . . . . . . . . . . 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 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔))
116	115	imp 407	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)
117	116	an32s 649	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑔)
118		snidg 4606	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
119	30, 118	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
120		elun2 4123	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)} → (𝑋 ∖ 𝑥) ∈ (𝐹 ∪ {(𝑋 ∖ 𝑥)}))
121	119, 120	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝐹 ∪ {(𝑋 ∖ 𝑥)}))
122	103, 121	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
123	122	adantlr 712	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
124	117, 123	sseldd 3932	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (𝑋 ∖ 𝑥) ∈ 𝑔)
125		simpllr 773	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑔 ∈ (UFil‘𝑋))
126		simprl 768	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → 𝑥 ⊆ 𝑋)
127		ufilb 23155	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝑔 ↔ (𝑋 ∖ 𝑥) ∈ 𝑔))
128	125, 126, 127	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → (¬ 𝑥 ∈ 𝑔 ↔ (𝑋 ∖ 𝑥) ∈ 𝑔))
129	124, 128	mpbird 256	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹)) → ¬ 𝑥 ∈ 𝑔)
130	129	expr 457	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ 𝑔))
131	130	con4d 115	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹))
132	131	ex 413	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹)))
133	132	com23 86	. . . . . . . 8 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → (𝑥 ⊆ 𝑋 → 𝑥 ∈ 𝐹)))
134	24, 133	mpdd 43	. . . . . . 7 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → (𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹))
135	134	ssrdv 3937	. . . . . 6 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝑔 ⊆ 𝐹)
136	19, 135	eqssd 3948	. . . . 5 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 = 𝑔)
137		simplr 766	. . . . 5 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝑔 ∈ (UFil‘𝑋))
138	136, 137	eqeltrd 2837	. . . 4 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑔 ∈ (UFil‘𝑋)) ∧ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔)) → 𝐹 ∈ (UFil‘𝑋))
139	138	rexlimdva2 3150	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃𝑔 ∈ (UFil‘𝑋)∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔) → 𝐹 ∈ (UFil‘𝑋)))
140	13, 139	biimtrid 241	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 → 𝐹 ∈ (UFil‘𝑋)))
141	12, 140	impbid2 225	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ (UFil‘𝑋) ↔ ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  ∃!wreu 3347  Vcvv 3441   ∖ cdif 3894   ∪ cun 3895   ∩ cin 3896   ⊆ wss 3897  ∅c0 4268  𝒫 cpw 4546  {csn 4572  ‘cfv 6473  (class class class)co 7329  ficfi 9259  fBascfbas 20683  filGencfg 20684  Filcfil 23094  UFilcufil 23148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-ac2 10312

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-int 4894  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-se 5570  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-isom 6482  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-rpss 7630  df-om 7773  df-1st 7891  df-2nd 7892  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-1o 8359  df-oadd 8363  df-er 8561  df-en 8797  df-dom 8798  df-fin 8800  df-fi 9260  df-dju 9750  df-card 9788  df-ac 9965  df-fbas 20692  df-fg 20693  df-fil 23095  df-ufil 23150

This theorem is referenced by: (None)