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

Theorem filufint 21944
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 3354 . . . . 5 𝑥 ∈ V
21elintrab 4623 . . . 4 (𝑥 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} ↔ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓))
3 filsspw 21875 . . . . . . . . . . . . . 14 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
433ad2ant1 1127 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ 𝒫 𝑋)
5 difss 3888 . . . . . . . . . . . . . . 15 (𝑋𝑥) ⊆ 𝑋
6 filtop 21879 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
7 difexg 4942 . . . . . . . . . . . . . . . . . 18 (𝑋𝐹 → (𝑋𝑥) ∈ V)
86, 7syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Fil‘𝑋) → (𝑋𝑥) ∈ V)
983ad2ant1 1127 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ V)
10 elpwg 4305 . . . . . . . . . . . . . . . 16 ((𝑋𝑥) ∈ V → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
119, 10syl 17 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
125, 11mpbiri 248 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ 𝒫 𝑋)
1312snssd 4475 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ⊆ 𝒫 𝑋)
144, 13unssd 3940 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋)
15 ssun1 3927 . . . . . . . . . . . . . 14 𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)})
16 filn0 21886 . . . . . . . . . . . . . 14 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
17 ssn0 4120 . . . . . . . . . . . . . 14 ((𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
1815, 16, 17sylancr 575 . . . . . . . . . . . . 13 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
19183ad2ant1 1127 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
20 elsni 4333 . . . . . . . . . . . . . . 15 (𝑧 ∈ {(𝑋𝑥)} → 𝑧 = (𝑋𝑥))
21 filelss 21876 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
22213adant3 1126 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → 𝑦𝑋)
23 reldisj 4163 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑋 → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋𝑥))))
2422, 23syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋𝑥))))
25 dfss4 4007 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝑋 ↔ (𝑋 ∖ (𝑋𝑥)) = 𝑥)
2625biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑋 → (𝑋 ∖ (𝑋𝑥)) = 𝑥)
2726sseq2d 3782 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝑋 → (𝑦 ⊆ (𝑋 ∖ (𝑋𝑥)) ↔ 𝑦𝑥))
28273ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (𝑦 ⊆ (𝑋 ∖ (𝑋𝑥)) ↔ 𝑦𝑥))
2924, 28bitrd 268 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦𝑥))
30 filss 21877 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑥𝑋𝑦𝑥)) → 𝑥𝐹)
31303exp2 1447 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → (𝑦𝐹 → (𝑥𝑋 → (𝑦𝑥𝑥𝐹))))
32313imp 1101 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (𝑦𝑥𝑥𝐹))
3329, 32sylbid 230 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ → 𝑥𝐹))
3433necon3bd 2957 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (¬ 𝑥𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))
35343exp 1112 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (Fil‘𝑋) → (𝑦𝐹 → (𝑥𝑋 → (¬ 𝑥𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))))
3635com24 95 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → (𝑥𝑋 → (𝑦𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))))
37363imp1 1440 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑦𝐹) → (𝑦 ∩ (𝑋𝑥)) ≠ ∅)
38 ineq2 3959 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑋𝑥) → (𝑦𝑧) = (𝑦 ∩ (𝑋𝑥)))
3938neeq1d 3002 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑋𝑥) → ((𝑦𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑋𝑥)) ≠ ∅))
4037, 39syl5ibrcom 237 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑦𝐹) → (𝑧 = (𝑋𝑥) → (𝑦𝑧) ≠ ∅))
4140expimpd 441 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑦𝐹𝑧 = (𝑋𝑥)) → (𝑦𝑧) ≠ ∅))
4220, 41sylan2i 593 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑦𝐹𝑧 ∈ {(𝑋𝑥)}) → (𝑦𝑧) ≠ ∅))
4342ralrimivv 3119 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅)
44 filfbas 21872 . . . . . . . . . . . . . . 15 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
45443ad2ant1 1127 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ∈ (fBas‘𝑋))
465a1i 11 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ⊆ 𝑋)
47263ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → (𝑋 ∖ (𝑋𝑥)) = 𝑥)
48 difeq2 3873 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝑥) = ∅ → (𝑋 ∖ (𝑋𝑥)) = (𝑋 ∖ ∅))
49 dif0 4097 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∖ ∅) = 𝑋
5048, 49syl6eq 2821 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝑥) = ∅ → (𝑋 ∖ (𝑋𝑥)) = 𝑋)
51503ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → (𝑋 ∖ (𝑋𝑥)) = 𝑋)
5247, 51eqtr3d 2807 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑥 = 𝑋)
5363ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑋𝐹)
5452, 53eqeltrd 2850 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑥𝐹)
55543expia 1114 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → ((𝑋𝑥) = ∅ → 𝑥𝐹))
5655necon3bd 2957 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → (¬ 𝑥𝐹 → (𝑋𝑥) ≠ ∅))
5756ex 397 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Fil‘𝑋) → (𝑥𝑋 → (¬ 𝑥𝐹 → (𝑋𝑥) ≠ ∅)))
5857com23 86 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → (𝑥𝑋 → (𝑋𝑥) ≠ ∅)))
59583imp 1101 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ≠ ∅)
6063ad2ant1 1127 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝑋𝐹)
61 snfbas 21890 . . . . . . . . . . . . . . 15 (((𝑋𝑥) ⊆ 𝑋 ∧ (𝑋𝑥) ≠ ∅ ∧ 𝑋𝐹) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
6246, 59, 60, 61syl3anc 1476 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
63 fbunfip 21893 . . . . . . . . . . . . . 14 ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅))
6445, 62, 63syl2anc 573 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅))
6543, 64mpbird 247 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
66 fsubbas 21891 . . . . . . . . . . . . . 14 (𝑋𝐹 → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
676, 66syl 17 . . . . . . . . . . . . 13 (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
68673ad2ant1 1127 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
6914, 19, 65, 68mpbir3and 1427 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋))
70 fgcl 21902 . . . . . . . . . . 11 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
7169, 70syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
72 filssufil 21936 . . . . . . . . . . 11 ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
73 snex 5036 . . . . . . . . . . . . . . . . . . . . 21 {(𝑋𝑥)} ∈ V
74 unexg 7106 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋𝑥)} ∈ V) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
7573, 74mpan2 671 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
76 ssfii 8481 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∪ {(𝑋𝑥)}) ∈ V → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
7775, 76syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
78773ad2ant1 1127 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
7978unssad 3941 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
80 ssfg 21896 . . . . . . . . . . . . . . . . . 18 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8169, 80syl 17 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8279, 81sstrd 3762 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8382ad2antrr 705 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
84 simpr 471 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
8583, 84sstrd 3762 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → 𝐹𝑓)
86 ufilfil 21928 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
87 0nelfil 21873 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
8886, 87syl 17 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (UFil‘𝑋) → ¬ ∅ ∈ 𝑓)
8988ad2antlr 706 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → ¬ ∅ ∈ 𝑓)
90 disjdif 4182 . . . . . . . . . . . . . . . . 17 (𝑥 ∩ (𝑋𝑥)) = ∅
9186ad2antlr 706 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → 𝑓 ∈ (Fil‘𝑋))
92 simprr 756 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → 𝑥𝑓)
9377unssbd 3942 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 ∈ (Fil‘𝑋) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
94933ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
9594adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
9669adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋))
9796, 80syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
9895, 97sstrd 3762 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
9998adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → {(𝑋𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
100 simprl 754 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
10199, 100sstrd 3762 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → {(𝑋𝑥)} ⊆ 𝑓)
102 snidg 4345 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝑥) ∈ V → (𝑋𝑥) ∈ {(𝑋𝑥)})
1038, 102syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Fil‘𝑋) → (𝑋𝑥) ∈ {(𝑋𝑥)})
1041033ad2ant1 1127 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ {(𝑋𝑥)})
105104ad2antrr 705 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋𝑥) ∈ {(𝑋𝑥)})
106101, 105sseldd 3753 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋𝑥) ∈ 𝑓)
107 filin 21878 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓 ∧ (𝑋𝑥) ∈ 𝑓) → (𝑥 ∩ (𝑋𝑥)) ∈ 𝑓)
10891, 92, 106, 107syl3anc 1476 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑥 ∩ (𝑋𝑥)) ∈ 𝑓)
10990, 108syl5eqelr 2855 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → ∅ ∈ 𝑓)
110109expr 444 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑥𝑓 → ∅ ∈ 𝑓))
11189, 110mtod 189 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → ¬ 𝑥𝑓)
11285, 111jca 501 . . . . . . . . . . . . 13 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝐹𝑓 ∧ ¬ 𝑥𝑓))
113112exp31 406 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑓 ∈ (UFil‘𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → (𝐹𝑓 ∧ ¬ 𝑥𝑓))))
114113reximdvai 3163 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
11572, 114syl5 34 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
11671, 115mpd 15 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓))
1171163expia 1114 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → (𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
118 filssufil 21936 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹𝑓)
119 filelss 21876 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓) → 𝑥𝑋)
120119ex 397 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (Fil‘𝑋) → (𝑥𝑓𝑥𝑋))
12186, 120syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ (UFil‘𝑋) → (𝑥𝑓𝑥𝑋))
122121con3d 149 . . . . . . . . . . . . . 14 (𝑓 ∈ (UFil‘𝑋) → (¬ 𝑥𝑋 → ¬ 𝑥𝑓))
123122impcom 394 . . . . . . . . . . . . 13 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → ¬ 𝑥𝑓)
124123a1d 25 . . . . . . . . . . . 12 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → (𝐹𝑓 → ¬ 𝑥𝑓))
125124ancld 540 . . . . . . . . . . 11 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → (𝐹𝑓 → (𝐹𝑓 ∧ ¬ 𝑥𝑓)))
126125reximdva 3165 . . . . . . . . . 10 𝑥𝑋 → (∃𝑓 ∈ (UFil‘𝑋)𝐹𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
127118, 126syl5com 31 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
128127adantr 466 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → (¬ 𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
129117, 128pm2.61d 171 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓))
130129ex 397 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
131 rexanali 3146 . . . . . 6 (∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓) ↔ ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓))
132130, 131syl6ib 241 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓)))
133132con4d 115 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓) → 𝑥𝐹))
1342, 133syl5bi 232 . . 3 (𝐹 ∈ (Fil‘𝑋) → (𝑥 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} → 𝑥𝐹))
135134ssrdv 3758 . 2 (𝐹 ∈ (Fil‘𝑋) → {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} ⊆ 𝐹)
136 ssintub 4629 . . 3 𝐹 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓}
137136a1i 11 . 2 (𝐹 ∈ (Fil‘𝑋) → 𝐹 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓})
138135, 137eqssd 3769 1 (𝐹 ∈ (Fil‘𝑋) → {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  cdif 3720  cun 3721  cin 3722  wss 3723  c0 4063  𝒫 cpw 4297  {csn 4316   cint 4611  cfv 6031  (class class class)co 6793  ficfi 8472  fBascfbas 19949  filGencfg 19950  Filcfil 21869  UFilcufil 21923
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-ac2 9487
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-rpss 7084  df-om 7213  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-en 8110  df-dom 8111  df-fin 8113  df-fi 8473  df-card 8965  df-ac 9139  df-cda 9192  df-fbas 19958  df-fg 19959  df-fil 21870  df-ufil 21925
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator