MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  filufint Structured version   Visualization version   GIF version

Theorem filufint 22456
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.
StepHypRef Expression
1 vex 3495 . . . . 5 𝑥 ∈ V
21elintrab 4879 . . . 4 (𝑥 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} ↔ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓))
3 filsspw 22387 . . . . . . . . . . . . . 14 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
433ad2ant1 1125 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ 𝒫 𝑋)
5 difss 4105 . . . . . . . . . . . . . . 15 (𝑋𝑥) ⊆ 𝑋
6 filtop 22391 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
7 difexg 5222 . . . . . . . . . . . . . . . . . 18 (𝑋𝐹 → (𝑋𝑥) ∈ V)
86, 7syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Fil‘𝑋) → (𝑋𝑥) ∈ V)
983ad2ant1 1125 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ V)
10 elpwg 4541 . . . . . . . . . . . . . . . 16 ((𝑋𝑥) ∈ V → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
119, 10syl 17 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
125, 11mpbiri 259 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ 𝒫 𝑋)
1312snssd 4734 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ⊆ 𝒫 𝑋)
144, 13unssd 4159 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋)
15 ssun1 4145 . . . . . . . . . . . . . 14 𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)})
16 filn0 22398 . . . . . . . . . . . . . 14 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
17 ssn0 4351 . . . . . . . . . . . . . 14 ((𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
1815, 16, 17sylancr 587 . . . . . . . . . . . . 13 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
19183ad2ant1 1125 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
20 elsni 4574 . . . . . . . . . . . . . . 15 (𝑧 ∈ {(𝑋𝑥)} → 𝑧 = (𝑋𝑥))
21 filelss 22388 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
22213adant3 1124 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → 𝑦𝑋)
23 reldisj 4398 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑋 → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋𝑥))))
2422, 23syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋𝑥))))
25 dfss4 4232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝑋 ↔ (𝑋 ∖ (𝑋𝑥)) = 𝑥)
2625biimpi 217 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑋 → (𝑋 ∖ (𝑋𝑥)) = 𝑥)
2726sseq2d 3996 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝑋 → (𝑦 ⊆ (𝑋 ∖ (𝑋𝑥)) ↔ 𝑦𝑥))
28273ad2ant3 1127 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (𝑦 ⊆ (𝑋 ∖ (𝑋𝑥)) ↔ 𝑦𝑥))
2924, 28bitrd 280 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦𝑥))
30 filss 22389 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑥𝑋𝑦𝑥)) → 𝑥𝐹)
31303exp2 1346 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → (𝑦𝐹 → (𝑥𝑋 → (𝑦𝑥𝑥𝐹))))
32313imp 1103 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (𝑦𝑥𝑥𝐹))
3329, 32sylbid 241 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ → 𝑥𝐹))
3433necon3bd 3027 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (¬ 𝑥𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))
35343exp 1111 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (Fil‘𝑋) → (𝑦𝐹 → (𝑥𝑋 → (¬ 𝑥𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))))
3635com24 95 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → (𝑥𝑋 → (𝑦𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))))
37363imp1 1339 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑦𝐹) → (𝑦 ∩ (𝑋𝑥)) ≠ ∅)
38 ineq2 4180 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑋𝑥) → (𝑦𝑧) = (𝑦 ∩ (𝑋𝑥)))
3938neeq1d 3072 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑋𝑥) → ((𝑦𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑋𝑥)) ≠ ∅))
4037, 39syl5ibrcom 248 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑦𝐹) → (𝑧 = (𝑋𝑥) → (𝑦𝑧) ≠ ∅))
4140expimpd 454 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑦𝐹𝑧 = (𝑋𝑥)) → (𝑦𝑧) ≠ ∅))
4220, 41sylan2i 605 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑦𝐹𝑧 ∈ {(𝑋𝑥)}) → (𝑦𝑧) ≠ ∅))
4342ralrimivv 3187 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅)
44 filfbas 22384 . . . . . . . . . . . . . . 15 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
45443ad2ant1 1125 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ∈ (fBas‘𝑋))
465a1i 11 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ⊆ 𝑋)
47263ad2ant2 1126 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → (𝑋 ∖ (𝑋𝑥)) = 𝑥)
48 difeq2 4090 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝑥) = ∅ → (𝑋 ∖ (𝑋𝑥)) = (𝑋 ∖ ∅))
49 dif0 4329 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∖ ∅) = 𝑋
5048, 49syl6eq 2869 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝑥) = ∅ → (𝑋 ∖ (𝑋𝑥)) = 𝑋)
51503ad2ant3 1127 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → (𝑋 ∖ (𝑋𝑥)) = 𝑋)
5247, 51eqtr3d 2855 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑥 = 𝑋)
5363ad2ant1 1125 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑋𝐹)
5452, 53eqeltrd 2910 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑥𝐹)
55543expia 1113 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → ((𝑋𝑥) = ∅ → 𝑥𝐹))
5655necon3bd 3027 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → (¬ 𝑥𝐹 → (𝑋𝑥) ≠ ∅))
5756ex 413 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Fil‘𝑋) → (𝑥𝑋 → (¬ 𝑥𝐹 → (𝑋𝑥) ≠ ∅)))
5857com23 86 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → (𝑥𝑋 → (𝑋𝑥) ≠ ∅)))
59583imp 1103 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ≠ ∅)
6063ad2ant1 1125 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝑋𝐹)
61 snfbas 22402 . . . . . . . . . . . . . . 15 (((𝑋𝑥) ⊆ 𝑋 ∧ (𝑋𝑥) ≠ ∅ ∧ 𝑋𝐹) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
6246, 59, 60, 61syl3anc 1363 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
63 fbunfip 22405 . . . . . . . . . . . . . 14 ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅))
6445, 62, 63syl2anc 584 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅))
6543, 64mpbird 258 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
66 fsubbas 22403 . . . . . . . . . . . . . 14 (𝑋𝐹 → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
676, 66syl 17 . . . . . . . . . . . . 13 (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
68673ad2ant1 1125 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
6914, 19, 65, 68mpbir3and 1334 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋))
70 fgcl 22414 . . . . . . . . . . 11 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
7169, 70syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
72 filssufil 22448 . . . . . . . . . . 11 ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
73 snex 5322 . . . . . . . . . . . . . . . . . . . . 21 {(𝑋𝑥)} ∈ V
74 unexg 7461 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋𝑥)} ∈ V) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
7573, 74mpan2 687 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
76 ssfii 8871 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∪ {(𝑋𝑥)}) ∈ V → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
7775, 76syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
78773ad2ant1 1125 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
7978unssad 4160 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
80 ssfg 22408 . . . . . . . . . . . . . . . . . 18 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8169, 80syl 17 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8279, 81sstrd 3974 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8382ad2antrr 722 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
84 simpr 485 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
8583, 84sstrd 3974 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → 𝐹𝑓)
86 ufilfil 22440 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
87 0nelfil 22385 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
8886, 87syl 17 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (UFil‘𝑋) → ¬ ∅ ∈ 𝑓)
8988ad2antlr 723 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → ¬ ∅ ∈ 𝑓)
90 disjdif 4417 . . . . . . . . . . . . . . . . 17 (𝑥 ∩ (𝑋𝑥)) = ∅
9186ad2antlr 723 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → 𝑓 ∈ (Fil‘𝑋))
92 simprr 769 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → 𝑥𝑓)
9377unssbd 4161 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 ∈ (Fil‘𝑋) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
94933ad2ant1 1125 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
9594adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
9669adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋))
9796, 80syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
9895, 97sstrd 3974 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
9998adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → {(𝑋𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
100 simprl 767 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
10199, 100sstrd 3974 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → {(𝑋𝑥)} ⊆ 𝑓)
102 snidg 4589 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝑥) ∈ V → (𝑋𝑥) ∈ {(𝑋𝑥)})
1038, 102syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Fil‘𝑋) → (𝑋𝑥) ∈ {(𝑋𝑥)})
1041033ad2ant1 1125 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ {(𝑋𝑥)})
105104ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋𝑥) ∈ {(𝑋𝑥)})
106101, 105sseldd 3965 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋𝑥) ∈ 𝑓)
107 filin 22390 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓 ∧ (𝑋𝑥) ∈ 𝑓) → (𝑥 ∩ (𝑋𝑥)) ∈ 𝑓)
10891, 92, 106, 107syl3anc 1363 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑥 ∩ (𝑋𝑥)) ∈ 𝑓)
10990, 108eqeltrrid 2915 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → ∅ ∈ 𝑓)
110109expr 457 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑥𝑓 → ∅ ∈ 𝑓))
11189, 110mtod 199 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → ¬ 𝑥𝑓)
11285, 111jca 512 . . . . . . . . . . . . 13 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝐹𝑓 ∧ ¬ 𝑥𝑓))
113112exp31 420 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑓 ∈ (UFil‘𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → (𝐹𝑓 ∧ ¬ 𝑥𝑓))))
114113reximdvai 3269 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
11572, 114syl5 34 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
11671, 115mpd 15 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓))
1171163expia 1113 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → (𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
118 filssufil 22448 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹𝑓)
119 filelss 22388 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓) → 𝑥𝑋)
120119ex 413 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (Fil‘𝑋) → (𝑥𝑓𝑥𝑋))
12186, 120syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ (UFil‘𝑋) → (𝑥𝑓𝑥𝑋))
122121con3d 155 . . . . . . . . . . . . . 14 (𝑓 ∈ (UFil‘𝑋) → (¬ 𝑥𝑋 → ¬ 𝑥𝑓))
123122impcom 408 . . . . . . . . . . . . 13 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → ¬ 𝑥𝑓)
124123a1d 25 . . . . . . . . . . . 12 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → (𝐹𝑓 → ¬ 𝑥𝑓))
125124ancld 551 . . . . . . . . . . 11 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → (𝐹𝑓 → (𝐹𝑓 ∧ ¬ 𝑥𝑓)))
126125reximdva 3271 . . . . . . . . . 10 𝑥𝑋 → (∃𝑓 ∈ (UFil‘𝑋)𝐹𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
127118, 126syl5com 31 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
128127adantr 481 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → (¬ 𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
129117, 128pm2.61d 180 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓))
130129ex 413 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
131 rexanali 3262 . . . . . 6 (∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓) ↔ ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓))
132130, 131syl6ib 252 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓)))
133132con4d 115 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓) → 𝑥𝐹))
1342, 133syl5bi 243 . . 3 (𝐹 ∈ (Fil‘𝑋) → (𝑥 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} → 𝑥𝐹))
135134ssrdv 3970 . 2 (𝐹 ∈ (Fil‘𝑋) → {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} ⊆ 𝐹)
136 ssintub 4885 . . 3 𝐹 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓}
137136a1i 11 . 2 (𝐹 ∈ (Fil‘𝑋) → 𝐹 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓})
138135, 137eqssd 3981 1 (𝐹 ∈ (Fil‘𝑋) → {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  {crab 3139  Vcvv 3492  cdif 3930  cun 3931  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535  {csn 4557   cint 4867  cfv 6348  (class class class)co 7145  ficfi 8862  fBascfbas 20461  filGencfg 20462  Filcfil 22381  UFilcufil 22435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-ac2 9873
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-rpss 7438  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-en 8498  df-dom 8499  df-fin 8501  df-fi 8863  df-dju 9318  df-card 9356  df-ac 9530  df-fbas 20470  df-fg 20471  df-fil 22382  df-ufil 22437
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator