Theorem filufint 22979

Description: A filter is equal to the intersection of the ultrafilters containing it. (Contributed by Jeff Hankins, 1-Jan-2010.) (Revised by Stefan O'Rear, 2-Aug-2015.)

Assertion

Ref	Expression
filufint	⊢ (𝐹 ∈ (Fil‘𝑋) → ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} = 𝐹)

Distinct variable groups:   𝑓,𝐹   𝑓,𝑋

Proof of Theorem filufint

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3426	. . . . 5 ⊢ 𝑥 ∈ V
2	1	elintrab 4888	. . . 4 ⊢ (𝑥 ∈ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} ↔ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓))
3		filsspw 22910	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
4	3	3ad2ant1 1131	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ 𝒫 𝑋)
5		difss 4062	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋
6		filtop 22914	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
7	6	difexd 5248	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋 ∖ 𝑥) ∈ V)
8	7	3ad2ant1 1131	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ V)
9		elpwg 4533	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∖ 𝑥) ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
10	8, 9	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
11	5, 10	mpbiri 257	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋)
12	11	snssd 4739	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ⊆ 𝒫 𝑋)
13	4, 12	unssd 4116	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋)
14		ssun1 4102	. . . . . . . . . . . . . 14 ⊢ 𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)})
15		filn0 22921	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
16		ssn0 4331	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
17	14, 15, 16	sylancr 586	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
18	17	3ad2ant1 1131	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
19		elsni 4575	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ {(𝑋 ∖ 𝑥)} → 𝑧 = (𝑋 ∖ 𝑥))
20		filelss 22911	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋)
21	20	3adant3 1130	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝑦 ⊆ 𝑋)
22		reldisj 4382	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ⊆ 𝑋 → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥))))
23	21, 22	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥))))
24		dfss4 4189	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥)
25	24	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ⊆ 𝑋 → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥)
26	25	sseq2d 3949	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ⊆ 𝑋 → (𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)) ↔ 𝑦 ⊆ 𝑥))
27	26	3ad2ant3 1133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)) ↔ 𝑦 ⊆ 𝑥))
28	23, 27	bitrd 278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ 𝑥))
29		filss 22912	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝐹)
30	29	3exp2 1352	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹))))
31	30	3imp 1109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹))
32	28, 31	sylbid 239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ → 𝑥 ∈ 𝐹))
33	32	necon3bd 2956	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
34	33	3exp 1117	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (¬ 𝑥 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))))
35	34	com24 95	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑦 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))))
36	35	3imp1 1345	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑦 ∈ 𝐹) → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)
37		ineq2 4137	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑋 ∖ 𝑥) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑋 ∖ 𝑥)))
38	37	neeq1d 3002	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑋 ∖ 𝑥) → ((𝑦 ∩ 𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
39	36, 38	syl5ibrcom 246	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑦 ∈ 𝐹) → (𝑧 = (𝑋 ∖ 𝑥) → (𝑦 ∩ 𝑧) ≠ ∅))
40	39	expimpd 453	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∈ 𝐹 ∧ 𝑧 = (𝑋 ∖ 𝑥)) → (𝑦 ∩ 𝑧) ≠ ∅))
41	19, 40	sylan2i 605	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {(𝑋 ∖ 𝑥)}) → (𝑦 ∩ 𝑧) ≠ ∅))
42	41	ralrimivv 3113	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅)
43		filfbas 22907	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
44	43	3ad2ant1 1131	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ∈ (fBas‘𝑋))
45	5	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ⊆ 𝑋)
46	25	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥)
47		difeq2 4047	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∖ 𝑥) = ∅ → (𝑋 ∖ (𝑋 ∖ 𝑥)) = (𝑋 ∖ ∅))
48		dif0 4303	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑋 ∖ ∅) = 𝑋
49	47, 48	eqtrdi 2795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋 ∖ 𝑥) = ∅ → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑋)
50	49	3ad2ant3 1133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑋)
51	46, 50	eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑥 = 𝑋)
52	6	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑋 ∈ 𝐹)
53	51, 52	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑥 ∈ 𝐹)
54	53	3expia 1119	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) = ∅ → 𝑥 ∈ 𝐹))
55	54	necon3bd 2956	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅))
56	55	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ⊆ 𝑋 → (¬ 𝑥 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅)))
57	56	com23 86	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑋 ∖ 𝑥) ≠ ∅)))
58	57	3imp 1109	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ≠ ∅)
59	6	3ad2ant1 1131	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝑋 ∈ 𝐹)
60		snfbas 22925	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅ ∧ 𝑋 ∈ 𝐹) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
61	45, 58, 59, 60	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
62		fbunfip 22928	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅))
63	44, 61, 62	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅))
64	42, 63	mpbird 256	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
65		fsubbas 22926	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
66	6, 65	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
67	66	3ad2ant1 1131	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
68	13, 18, 64, 67	mpbir3and 1340	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋))
69		fgcl 22937	. . . . . . . . . . 11 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
70	68, 69	syl 17	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
71		filssufil 22971	. . . . . . . . . . 11 ⊢ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
72		snex 5349	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {(𝑋 ∖ 𝑥)} ∈ V
73		unexg 7577	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ V) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
74	72, 73	mpan2 687	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
75		ssfii 9108	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
77	76	3ad2ant1 1131	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
78	77	unssad 4117	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
79		ssfg 22931	. . . . . . . . . . . . . . . . . 18 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
80	68, 79	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
81	78, 80	sstrd 3927	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
82	81	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
83		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
84	82, 83	sstrd 3927	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ 𝑓)
85		ufilfil 22963	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
86		0nelfil 22908	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
87	85, 86	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (UFil‘𝑋) → ¬ ∅ ∈ 𝑓)
88	87	ad2antlr 723	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ¬ ∅ ∈ 𝑓)
89		disjdif 4402	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∩ (𝑋 ∖ 𝑥)) = ∅
90	85	ad2antlr 723	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → 𝑓 ∈ (Fil‘𝑋))
91		simprr 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → 𝑥 ∈ 𝑓)
92	76	unssbd 4118	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 ∈ (Fil‘𝑋) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
93	92	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
94	93	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
95	68	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋))
96	95, 79	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
97	94, 96	sstrd 3927	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋 ∖ 𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
98	97	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → {(𝑋 ∖ 𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
99		simprl 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
100	98, 99	sstrd 3927	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → {(𝑋 ∖ 𝑥)} ⊆ 𝑓)
101		snidg 4592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
102	7, 101	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
103	102	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
104	103	ad2antrr 722	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
105	100, 104	sseldd 3918	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋 ∖ 𝑥) ∈ 𝑓)
106		filin 22913	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑓 ∧ (𝑋 ∖ 𝑥) ∈ 𝑓) → (𝑥 ∩ (𝑋 ∖ 𝑥)) ∈ 𝑓)
107	90, 91, 105, 106	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑥 ∩ (𝑋 ∖ 𝑥)) ∈ 𝑓)
108	89, 107	eqeltrrid 2844	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → ∅ ∈ 𝑓)
109	108	expr 456	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑥 ∈ 𝑓 → ∅ ∈ 𝑓))
110	88, 109	mtod 197	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ¬ 𝑥 ∈ 𝑓)
111	84, 110	jca 511	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))
112	111	exp31 419	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑓 ∈ (UFil‘𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))))
113	112	reximdvai 3199	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
114	71, 113	syl5 34	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
115	70, 114	mpd 15	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))
116	115	3expia 1119	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → (𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
117		filssufil 22971	. . . . . . . . . 10 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
118		filelss 22911	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋)
119	118	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋))
120	85, 119	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋))
121	120	con3d 152	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ (UFil‘𝑋) → (¬ 𝑥 ⊆ 𝑋 → ¬ 𝑥 ∈ 𝑓))
122	121	impcom 407	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → ¬ 𝑥 ∈ 𝑓)
123	122	a1d 25	. . . . . . . . . . . 12 ⊢ ((¬ 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → ¬ 𝑥 ∈ 𝑓))
124	123	ancld 550	. . . . . . . . . . 11 ⊢ ((¬ 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
125	124	reximdva 3202	. . . . . . . . . 10 ⊢ (¬ 𝑥 ⊆ 𝑋 → (∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
126	117, 125	syl5com 31	. . . . . . . . 9 ⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
127	126	adantr 480	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → (¬ 𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
128	116, 127	pm2.61d 179	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))
129	128	ex 412	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
130		rexanali 3191	. . . . . 6 ⊢ (∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓) ↔ ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓))
131	129, 130	syl6ib 250	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓)))
132	131	con4d 115	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓) → 𝑥 ∈ 𝐹))
133	2, 132	syl5bi 241	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ∈ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} → 𝑥 ∈ 𝐹))
134	133	ssrdv 3923	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} ⊆ 𝐹)
135		ssintub 4894	. . 3 ⊢ 𝐹 ⊆ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓}
136	135	a1i 11	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓})
137	134, 136	eqssd 3934	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} = 𝐹)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  {crab 3067  Vcvv 3422   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530  {csn 4558  ∩ cint 4876  ‘cfv 6418  (class class class)co 7255  ficfi 9099  fBascfbas 20498  filGencfg 20499  Filcfil 22904  UFilcufil 22958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-ac2 10150

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-rpss 7554  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-oadd 8271  df-er 8456  df-en 8692  df-dom 8693  df-fin 8695  df-fi 9100  df-dju 9590  df-card 9628  df-ac 9803  df-fbas 20507  df-fg 20508  df-fil 22905  df-ufil 22960

This theorem is referenced by: (None)