Theorem filufint 24045

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 3467	. . . . 5 ⊢ 𝑥 ∈ V
2	1	elintrab 4929	. . . 4 ⊢ (𝑥 ∈ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} ↔ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓))
3		filsspw 23976	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
4	3	3ad2ant1 1149	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ 𝒫 𝑋)
5		difss 4098	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋
6		filtop 23980	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
7	6	difexd 5302	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋 ∖ 𝑥) ∈ V)
8	7	3ad2ant1 1149	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ V)
9		elpwg 4570	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∖ 𝑥) ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
10	8, 9	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋))
11	5, 10	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋)
12	11	snssd 4757	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ⊆ 𝒫 𝑋)
13	4, 12	unssd 4153	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋)
14		ssun1 4139	. . . . . . . . . . . . . 14 ⊢ 𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)})
15		filn0 23987	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
16		ssn0 4368	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
17	14, 15, 16	sylancr 598	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
18	17	3ad2ant1 1149	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅)
19		elsni 4611	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ {(𝑋 ∖ 𝑥)} → 𝑧 = (𝑋 ∖ 𝑥))
20		filelss 23977	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋)
21	20	3adant3 1148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝑦 ⊆ 𝑋)
22		reldisj 4419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ⊆ 𝑋 → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥))))
23	21, 22	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥))))
24		dfss4 4230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥)
25	24	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ⊆ 𝑋 → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥)
26	25	sseq2d 3977	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ⊆ 𝑋 → (𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)) ↔ 𝑦 ⊆ 𝑥))
27	26	3ad2ant3 1151	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)) ↔ 𝑦 ⊆ 𝑥))
28	23, 27	bitrd 282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ 𝑥))
29		filss 23978	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝐹)
30	29	3exp2 1371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹))))
31	30	3imp 1126	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹))
32	28, 31	sylbid 243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ → 𝑥 ∈ 𝐹))
33	32	necon3bd 2978	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
34	33	3exp 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (¬ 𝑥 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))))
35	34	com24 96	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑦 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))))
36	35	3imp1 1364	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑦 ∈ 𝐹) → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)
37		ineq2 4175	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑋 ∖ 𝑥) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑋 ∖ 𝑥)))
38	37	neeq1d 3023	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑋 ∖ 𝑥) → ((𝑦 ∩ 𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅))
39	36, 38	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑦 ∈ 𝐹) → (𝑧 = (𝑋 ∖ 𝑥) → (𝑦 ∩ 𝑧) ≠ ∅))
40	39	expimpd 458	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∈ 𝐹 ∧ 𝑧 = (𝑋 ∖ 𝑥)) → (𝑦 ∩ 𝑧) ≠ ∅))
41	19, 40	sylan2i 617	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {(𝑋 ∖ 𝑥)}) → (𝑦 ∩ 𝑧) ≠ ∅))
42	41	ralrimivv 3212	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅)
43		filfbas 23973	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
44	43	3ad2ant1 1149	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ∈ (fBas‘𝑋))
45	5	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ⊆ 𝑋)
46	25	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥)
47		difeq2 4083	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∖ 𝑥) = ∅ → (𝑋 ∖ (𝑋 ∖ 𝑥)) = (𝑋 ∖ ∅))
48		dif0 4341	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑋 ∖ ∅) = 𝑋
49	47, 48	eqtrdi 2820	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋 ∖ 𝑥) = ∅ → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑋)
50	49	3ad2ant3 1151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑋)
51	46, 50	eqtr3d 2806	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑥 = 𝑋)
52	6	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑋 ∈ 𝐹)
53	51, 52	eqeltrd 2869	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑥 ∈ 𝐹)
54	53	3expia 1137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) = ∅ → 𝑥 ∈ 𝐹))
55	54	necon3bd 2978	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅))
56	55	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ⊆ 𝑋 → (¬ 𝑥 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅)))
57	56	com23 87	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑋 ∖ 𝑥) ≠ ∅)))
58	57	3imp 1126	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ≠ ∅)
59	6	3ad2ant1 1149	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝑋 ∈ 𝐹)
60		snfbas 23991	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅ ∧ 𝑋 ∈ 𝐹) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
61	45, 58, 59, 60	syl3anc 1396	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋))
62		fbunfip 23994	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅))
63	44, 61, 62	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅))
64	42, 63	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
65		fsubbas 23992	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
66	6, 65	syl 18	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
67	66	3ad2ant1 1149	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))))
68	13, 18, 64, 67	mpbir3and 1359	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋))
69		fgcl 24003	. . . . . . . . . . 11 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
70	68, 69	syl 18	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋))
71		filssufil 24037	. . . . . . . . . . 11 ⊢ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
72		snex 5411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {(𝑋 ∖ 𝑥)} ∈ V
73		unexg 7741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ V) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
74	72, 73	mpan2 703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V)
75		ssfii 9378	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
76	74, 75	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
77	76	3ad2ant1 1149	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
78	77	unssad 4154	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
79		ssfg 23997	. . . . . . . . . . . . . . . . . 18 ⊢ ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
80	68, 79	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
81	78, 80	sstrd 3955	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
82	81	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
83		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
84	82, 83	sstrd 3955	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ 𝑓)
85		ufilfil 24029	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
86		0nelfil 23974	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
87	85, 86	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (UFil‘𝑋) → ¬ ∅ ∈ 𝑓)
88	87	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ¬ ∅ ∈ 𝑓)
89		disjdif 4438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∩ (𝑋 ∖ 𝑥)) = ∅
90	85	ad2antlr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → 𝑓 ∈ (Fil‘𝑋))
91		simprr 784	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → 𝑥 ∈ 𝑓)
92	76	unssbd 4155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 ∈ (Fil‘𝑋) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
93	92	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
94	93	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))
95	68	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋))
96	95, 79	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
97	94, 96	sstrd 3955	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋 ∖ 𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
98	97	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → {(𝑋 ∖ 𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))
99		simprl 782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓)
100	98, 99	sstrd 3955	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → {(𝑋 ∖ 𝑥)} ⊆ 𝑓)
101		snidg 4631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∖ 𝑥) ∈ V → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
102	7, 101	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
103	102	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
104	103	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)})
105	100, 104	sseldd 3946	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋 ∖ 𝑥) ∈ 𝑓)
106		filin 23979	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑓 ∧ (𝑋 ∖ 𝑥) ∈ 𝑓) → (𝑥 ∩ (𝑋 ∖ 𝑥)) ∈ 𝑓)
107	90, 91, 105, 106	syl3anc 1396	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑥 ∩ (𝑋 ∖ 𝑥)) ∈ 𝑓)
108	89, 107	eqeltrrid 2874	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → ∅ ∈ 𝑓)
109	108	expr 461	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑥 ∈ 𝑓 → ∅ ∈ 𝑓))
110	88, 109	mtod 201	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ¬ 𝑥 ∈ 𝑓)
111	84, 110	jca 520	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))
112	111	exp31 424	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑓 ∈ (UFil‘𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))))
113	112	reximdvai 3182	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
114	71, 113	syl5 35	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
115	70, 114	mpd 16	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))
116	115	3expia 1137	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → (𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
117		filssufil 24037	. . . . . . . . . 10 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
118		filelss 23977	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋)
119	118	ex 417	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋))
120	85, 119	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋))
121	120	con3d 153	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ (UFil‘𝑋) → (¬ 𝑥 ⊆ 𝑋 → ¬ 𝑥 ∈ 𝑓))
122	121	impcom 412	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → ¬ 𝑥 ∈ 𝑓)
123	122	a1d 26	. . . . . . . . . . . 12 ⊢ ((¬ 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → ¬ 𝑥 ∈ 𝑓))
124	123	ancld 559	. . . . . . . . . . 11 ⊢ ((¬ 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
125	124	reximdva 3184	. . . . . . . . . 10 ⊢ (¬ 𝑥 ⊆ 𝑋 → (∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
126	117, 125	syl5com 32	. . . . . . . . 9 ⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
127	126	adantr 485	. . . . . . . 8 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → (¬ 𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
128	116, 127	pm2.61d 181	. . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))
129	128	ex 417	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))
130		rexanali 3125	. . . . . 6 ⊢ (∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓) ↔ ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓))
131	129, 130	imbitrdi 254	. . . . 5 ⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓)))
132	131	con4d 116	. . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓) → 𝑥 ∈ 𝐹))
133	2, 132	biimtrid 245	. . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ∈ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} → 𝑥 ∈ 𝐹))
134	133	ssrdv 3951	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} ⊆ 𝐹)
135		ssintub 4935	. . 3 ⊢ 𝐹 ⊆ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓}
136	135	a1i 11	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓})
137	134, 136	eqssd 3962	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} = 𝐹)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃wrex 3095  {crab 3423  Vcvv 3463   ∖ cdif 3910   ∪ cun 3911   ∩ cin 3912   ⊆ wss 3913  ∅c0 4294  𝒫 cpw 4567  {csn 4594  ∩ cint 4916  ‘cfv 6537  (class class class)co 7411  ficfi 9369  fBascfbas 21478  filGencfg 21479  Filcfil 23970  UFilcufil 24024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-ac2 10446

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-rpss 7721  df-om 7862  df-1st 7985  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8452  df-2o 8453  df-oadd 8456  df-er 8693  df-en 8943  df-dom 8944  df-fin 8946  df-fi 9370  df-dju 9886  df-card 9924  df-ac 10099  df-fbas 21487  df-fg 21488  df-fil 23971  df-ufil 24026

This theorem is referenced by: (None)