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

Theorem filufint 23929
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 3483 . . . . 5 𝑥 ∈ V
21elintrab 4959 . . . 4 (𝑥 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} ↔ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓))
3 filsspw 23860 . . . . . . . . . . . . . 14 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
433ad2ant1 1133 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ 𝒫 𝑋)
5 difss 4135 . . . . . . . . . . . . . . 15 (𝑋𝑥) ⊆ 𝑋
6 filtop 23864 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
76difexd 5330 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Fil‘𝑋) → (𝑋𝑥) ∈ V)
873ad2ant1 1133 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ V)
9 elpwg 4602 . . . . . . . . . . . . . . . 16 ((𝑋𝑥) ∈ V → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
108, 9syl 17 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
115, 10mpbiri 258 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ 𝒫 𝑋)
1211snssd 4808 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ⊆ 𝒫 𝑋)
134, 12unssd 4191 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋)
14 ssun1 4177 . . . . . . . . . . . . . 14 𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)})
15 filn0 23871 . . . . . . . . . . . . . 14 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
16 ssn0 4403 . . . . . . . . . . . . . 14 ((𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
1714, 15, 16sylancr 587 . . . . . . . . . . . . 13 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
18173ad2ant1 1133 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
19 elsni 4642 . . . . . . . . . . . . . . 15 (𝑧 ∈ {(𝑋𝑥)} → 𝑧 = (𝑋𝑥))
20 filelss 23861 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
21203adant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → 𝑦𝑋)
22 reldisj 4452 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑋 → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋𝑥))))
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋𝑥))))
24 dfss4 4268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝑋 ↔ (𝑋 ∖ (𝑋𝑥)) = 𝑥)
2524biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑋 → (𝑋 ∖ (𝑋𝑥)) = 𝑥)
2625sseq2d 4015 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝑋 → (𝑦 ⊆ (𝑋 ∖ (𝑋𝑥)) ↔ 𝑦𝑥))
27263ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (𝑦 ⊆ (𝑋 ∖ (𝑋𝑥)) ↔ 𝑦𝑥))
2823, 27bitrd 279 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦𝑥))
29 filss 23862 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑥𝑋𝑦𝑥)) → 𝑥𝐹)
30293exp2 1354 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → (𝑦𝐹 → (𝑥𝑋 → (𝑦𝑥𝑥𝐹))))
31303imp 1110 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (𝑦𝑥𝑥𝐹))
3228, 31sylbid 240 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ → 𝑥𝐹))
3332necon3bd 2953 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (¬ 𝑥𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))
34333exp 1119 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (Fil‘𝑋) → (𝑦𝐹 → (𝑥𝑋 → (¬ 𝑥𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))))
3534com24 95 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → (𝑥𝑋 → (𝑦𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))))
36353imp1 1347 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑦𝐹) → (𝑦 ∩ (𝑋𝑥)) ≠ ∅)
37 ineq2 4213 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑋𝑥) → (𝑦𝑧) = (𝑦 ∩ (𝑋𝑥)))
3837neeq1d 2999 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑋𝑥) → ((𝑦𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑋𝑥)) ≠ ∅))
3936, 38syl5ibrcom 247 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑦𝐹) → (𝑧 = (𝑋𝑥) → (𝑦𝑧) ≠ ∅))
4039expimpd 453 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑦𝐹𝑧 = (𝑋𝑥)) → (𝑦𝑧) ≠ ∅))
4119, 40sylan2i 606 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑦𝐹𝑧 ∈ {(𝑋𝑥)}) → (𝑦𝑧) ≠ ∅))
4241ralrimivv 3199 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅)
43 filfbas 23857 . . . . . . . . . . . . . . 15 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
44433ad2ant1 1133 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ∈ (fBas‘𝑋))
455a1i 11 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ⊆ 𝑋)
46253ad2ant2 1134 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → (𝑋 ∖ (𝑋𝑥)) = 𝑥)
47 difeq2 4119 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝑥) = ∅ → (𝑋 ∖ (𝑋𝑥)) = (𝑋 ∖ ∅))
48 dif0 4377 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∖ ∅) = 𝑋
4947, 48eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝑥) = ∅ → (𝑋 ∖ (𝑋𝑥)) = 𝑋)
50493ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → (𝑋 ∖ (𝑋𝑥)) = 𝑋)
5146, 50eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑥 = 𝑋)
5263ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑋𝐹)
5351, 52eqeltrd 2840 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑥𝐹)
54533expia 1121 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → ((𝑋𝑥) = ∅ → 𝑥𝐹))
5554necon3bd 2953 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → (¬ 𝑥𝐹 → (𝑋𝑥) ≠ ∅))
5655ex 412 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Fil‘𝑋) → (𝑥𝑋 → (¬ 𝑥𝐹 → (𝑋𝑥) ≠ ∅)))
5756com23 86 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → (𝑥𝑋 → (𝑋𝑥) ≠ ∅)))
58573imp 1110 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ≠ ∅)
5963ad2ant1 1133 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝑋𝐹)
60 snfbas 23875 . . . . . . . . . . . . . . 15 (((𝑋𝑥) ⊆ 𝑋 ∧ (𝑋𝑥) ≠ ∅ ∧ 𝑋𝐹) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
6145, 58, 59, 60syl3anc 1372 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
62 fbunfip 23878 . . . . . . . . . . . . . 14 ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅))
6344, 61, 62syl2anc 584 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅))
6442, 63mpbird 257 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
65 fsubbas 23876 . . . . . . . . . . . . . 14 (𝑋𝐹 → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
666, 65syl 17 . . . . . . . . . . . . 13 (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
67663ad2ant1 1133 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
6813, 18, 64, 67mpbir3and 1342 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋))
69 fgcl 23887 . . . . . . . . . . 11 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
7068, 69syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
71 filssufil 23921 . . . . . . . . . . 11 ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
72 snex 5435 . . . . . . . . . . . . . . . . . . . . 21 {(𝑋𝑥)} ∈ V
73 unexg 7764 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋𝑥)} ∈ V) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
7472, 73mpan2 691 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
75 ssfii 9460 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∪ {(𝑋𝑥)}) ∈ V → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
7674, 75syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
77763ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
7877unssad 4192 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
79 ssfg 23881 . . . . . . . . . . . . . . . . . 18 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8068, 79syl 17 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8178, 80sstrd 3993 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8281ad2antrr 726 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
83 simpr 484 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
8482, 83sstrd 3993 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → 𝐹𝑓)
85 ufilfil 23913 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
86 0nelfil 23858 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
8785, 86syl 17 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (UFil‘𝑋) → ¬ ∅ ∈ 𝑓)
8887ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → ¬ ∅ ∈ 𝑓)
89 disjdif 4471 . . . . . . . . . . . . . . . . 17 (𝑥 ∩ (𝑋𝑥)) = ∅
9085ad2antlr 727 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → 𝑓 ∈ (Fil‘𝑋))
91 simprr 772 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → 𝑥𝑓)
9276unssbd 4193 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 ∈ (Fil‘𝑋) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
93923ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
9493adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
9568adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋))
9695, 79syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
9794, 96sstrd 3993 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
9897adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → {(𝑋𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
99 simprl 770 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
10098, 99sstrd 3993 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → {(𝑋𝑥)} ⊆ 𝑓)
101 snidg 4659 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝑥) ∈ V → (𝑋𝑥) ∈ {(𝑋𝑥)})
1027, 101syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Fil‘𝑋) → (𝑋𝑥) ∈ {(𝑋𝑥)})
1031023ad2ant1 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ {(𝑋𝑥)})
104103ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋𝑥) ∈ {(𝑋𝑥)})
105100, 104sseldd 3983 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋𝑥) ∈ 𝑓)
106 filin 23863 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓 ∧ (𝑋𝑥) ∈ 𝑓) → (𝑥 ∩ (𝑋𝑥)) ∈ 𝑓)
10790, 91, 105, 106syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑥 ∩ (𝑋𝑥)) ∈ 𝑓)
10889, 107eqeltrrid 2845 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → ∅ ∈ 𝑓)
109108expr 456 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑥𝑓 → ∅ ∈ 𝑓))
11088, 109mtod 198 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → ¬ 𝑥𝑓)
11184, 110jca 511 . . . . . . . . . . . . 13 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝐹𝑓 ∧ ¬ 𝑥𝑓))
112111exp31 419 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑓 ∈ (UFil‘𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → (𝐹𝑓 ∧ ¬ 𝑥𝑓))))
113112reximdvai 3164 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
11471, 113syl5 34 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
11570, 114mpd 15 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓))
1161153expia 1121 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → (𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
117 filssufil 23921 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹𝑓)
118 filelss 23861 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓) → 𝑥𝑋)
119118ex 412 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (Fil‘𝑋) → (𝑥𝑓𝑥𝑋))
12085, 119syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ (UFil‘𝑋) → (𝑥𝑓𝑥𝑋))
121120con3d 152 . . . . . . . . . . . . . 14 (𝑓 ∈ (UFil‘𝑋) → (¬ 𝑥𝑋 → ¬ 𝑥𝑓))
122121impcom 407 . . . . . . . . . . . . 13 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → ¬ 𝑥𝑓)
123122a1d 25 . . . . . . . . . . . 12 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → (𝐹𝑓 → ¬ 𝑥𝑓))
124123ancld 550 . . . . . . . . . . 11 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → (𝐹𝑓 → (𝐹𝑓 ∧ ¬ 𝑥𝑓)))
125124reximdva 3167 . . . . . . . . . 10 𝑥𝑋 → (∃𝑓 ∈ (UFil‘𝑋)𝐹𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
126117, 125syl5com 31 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
127126adantr 480 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → (¬ 𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
128116, 127pm2.61d 179 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓))
129128ex 412 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
130 rexanali 3101 . . . . . 6 (∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓) ↔ ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓))
131129, 130imbitrdi 251 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓)))
132131con4d 115 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓) → 𝑥𝐹))
1332, 132biimtrid 242 . . 3 (𝐹 ∈ (Fil‘𝑋) → (𝑥 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} → 𝑥𝐹))
134133ssrdv 3988 . 2 (𝐹 ∈ (Fil‘𝑋) → {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} ⊆ 𝐹)
135 ssintub 4965 . . 3 𝐹 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓}
136135a1i 11 . 2 (𝐹 ∈ (Fil‘𝑋) → 𝐹 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓})
137134, 136eqssd 4000 1 (𝐹 ∈ (Fil‘𝑋) → {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wcel 2107  wne 2939  wral 3060  wrex 3069  {crab 3435  Vcvv 3479  cdif 3947  cun 3948  cin 3949  wss 3950  c0 4332  𝒫 cpw 4599  {csn 4625   cint 4945  cfv 6560  (class class class)co 7432  ficfi 9451  fBascfbas 21353  filGencfg 21354  Filcfil 23854  UFilcufil 23908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-ac2 10504
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-rpss 7744  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-oadd 8511  df-er 8746  df-en 8987  df-dom 8988  df-fin 8990  df-fi 9452  df-dju 9942  df-card 9980  df-ac 10157  df-fbas 21362  df-fg 21363  df-fil 23855  df-ufil 23910
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator