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

Theorem filufint 21634
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 3189 . . . . 5 𝑥 ∈ V
21elintrab 4453 . . . 4 (𝑥 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} ↔ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓))
3 filsspw 21565 . . . . . . . . . . . . . 14 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
433ad2ant1 1080 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ 𝒫 𝑋)
5 difss 3715 . . . . . . . . . . . . . . 15 (𝑋𝑥) ⊆ 𝑋
6 filtop 21569 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
7 difexg 4768 . . . . . . . . . . . . . . . . . 18 (𝑋𝐹 → (𝑋𝑥) ∈ V)
86, 7syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Fil‘𝑋) → (𝑋𝑥) ∈ V)
983ad2ant1 1080 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ V)
10 elpwg 4138 . . . . . . . . . . . . . . . 16 ((𝑋𝑥) ∈ V → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
119, 10syl 17 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
125, 11mpbiri 248 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ 𝒫 𝑋)
1312snssd 4309 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ⊆ 𝒫 𝑋)
144, 13unssd 3767 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋)
15 ssun1 3754 . . . . . . . . . . . . . 14 𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)})
16 filn0 21576 . . . . . . . . . . . . . 14 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
17 ssn0 3948 . . . . . . . . . . . . . 14 ((𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
1815, 16, 17sylancr 694 . . . . . . . . . . . . 13 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
19183ad2ant1 1080 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
20 elsni 4165 . . . . . . . . . . . . . . 15 (𝑧 ∈ {(𝑋𝑥)} → 𝑧 = (𝑋𝑥))
21 filelss 21566 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
22213adant3 1079 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → 𝑦𝑋)
23 reldisj 3992 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑋 → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋𝑥))))
2422, 23syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋𝑥))))
25 dfss4 3836 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝑋 ↔ (𝑋 ∖ (𝑋𝑥)) = 𝑥)
2625biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑋 → (𝑋 ∖ (𝑋𝑥)) = 𝑥)
2726sseq2d 3612 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝑋 → (𝑦 ⊆ (𝑋 ∖ (𝑋𝑥)) ↔ 𝑦𝑥))
28273ad2ant3 1082 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (𝑦 ⊆ (𝑋 ∖ (𝑋𝑥)) ↔ 𝑦𝑥))
2924, 28bitrd 268 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦𝑥))
30 filss 21567 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑥𝑋𝑦𝑥)) → 𝑥𝐹)
31303exp2 1282 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → (𝑦𝐹 → (𝑥𝑋 → (𝑦𝑥𝑥𝐹))))
32313imp 1254 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (𝑦𝑥𝑥𝐹))
3329, 32sylbid 230 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ → 𝑥𝐹))
3433necon3bd 2804 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (¬ 𝑥𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))
35343exp 1261 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (Fil‘𝑋) → (𝑦𝐹 → (𝑥𝑋 → (¬ 𝑥𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))))
3635com24 95 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → (𝑥𝑋 → (𝑦𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))))
37363imp1 1277 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑦𝐹) → (𝑦 ∩ (𝑋𝑥)) ≠ ∅)
38 ineq2 3786 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑋𝑥) → (𝑦𝑧) = (𝑦 ∩ (𝑋𝑥)))
3938neeq1d 2849 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑋𝑥) → ((𝑦𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑋𝑥)) ≠ ∅))
4037, 39syl5ibrcom 237 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑦𝐹) → (𝑧 = (𝑋𝑥) → (𝑦𝑧) ≠ ∅))
4140expimpd 628 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑦𝐹𝑧 = (𝑋𝑥)) → (𝑦𝑧) ≠ ∅))
4220, 41sylan2i 686 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑦𝐹𝑧 ∈ {(𝑋𝑥)}) → (𝑦𝑧) ≠ ∅))
4342ralrimivv 2964 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅)
44 filfbas 21562 . . . . . . . . . . . . . . 15 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
45443ad2ant1 1080 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ∈ (fBas‘𝑋))
465a1i 11 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ⊆ 𝑋)
47263ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → (𝑋 ∖ (𝑋𝑥)) = 𝑥)
48 difeq2 3700 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝑥) = ∅ → (𝑋 ∖ (𝑋𝑥)) = (𝑋 ∖ ∅))
49 dif0 3924 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∖ ∅) = 𝑋
5048, 49syl6eq 2671 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝑥) = ∅ → (𝑋 ∖ (𝑋𝑥)) = 𝑋)
51503ad2ant3 1082 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → (𝑋 ∖ (𝑋𝑥)) = 𝑋)
5247, 51eqtr3d 2657 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑥 = 𝑋)
5363ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑋𝐹)
5452, 53eqeltrd 2698 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑥𝐹)
55543expia 1264 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → ((𝑋𝑥) = ∅ → 𝑥𝐹))
5655necon3bd 2804 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → (¬ 𝑥𝐹 → (𝑋𝑥) ≠ ∅))
5756ex 450 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Fil‘𝑋) → (𝑥𝑋 → (¬ 𝑥𝐹 → (𝑋𝑥) ≠ ∅)))
5857com23 86 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → (𝑥𝑋 → (𝑋𝑥) ≠ ∅)))
59583imp 1254 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ≠ ∅)
6063ad2ant1 1080 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝑋𝐹)
61 snfbas 21580 . . . . . . . . . . . . . . 15 (((𝑋𝑥) ⊆ 𝑋 ∧ (𝑋𝑥) ≠ ∅ ∧ 𝑋𝐹) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
6246, 59, 60, 61syl3anc 1323 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
63 fbunfip 21583 . . . . . . . . . . . . . 14 ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅))
6445, 62, 63syl2anc 692 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅))
6543, 64mpbird 247 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
66 fsubbas 21581 . . . . . . . . . . . . . 14 (𝑋𝐹 → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
676, 66syl 17 . . . . . . . . . . . . 13 (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
68673ad2ant1 1080 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
6914, 19, 65, 68mpbir3and 1243 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋))
70 fgcl 21592 . . . . . . . . . . 11 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
7169, 70syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
72 filssufil 21626 . . . . . . . . . . 11 ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
73 snex 4869 . . . . . . . . . . . . . . . . . . . . 21 {(𝑋𝑥)} ∈ V
74 unexg 6912 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋𝑥)} ∈ V) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
7573, 74mpan2 706 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
76 ssfii 8269 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∪ {(𝑋𝑥)}) ∈ V → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
7775, 76syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
78773ad2ant1 1080 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
7978unssad 3768 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
80 ssfg 21586 . . . . . . . . . . . . . . . . . 18 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8169, 80syl 17 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8279, 81sstrd 3593 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8382ad2antrr 761 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
84 simpr 477 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
8583, 84sstrd 3593 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → 𝐹𝑓)
86 ufilfil 21618 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
87 0nelfil 21563 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
8886, 87syl 17 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (UFil‘𝑋) → ¬ ∅ ∈ 𝑓)
8988ad2antlr 762 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → ¬ ∅ ∈ 𝑓)
90 disjdif 4012 . . . . . . . . . . . . . . . . 17 (𝑥 ∩ (𝑋𝑥)) = ∅
9186ad2antlr 762 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → 𝑓 ∈ (Fil‘𝑋))
92 simprr 795 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → 𝑥𝑓)
9377unssbd 3769 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 ∈ (Fil‘𝑋) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
94933ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . 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 3593 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
9998adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → {(𝑋𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
100 simprl 793 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
10199, 100sstrd 3593 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → {(𝑋𝑥)} ⊆ 𝑓)
102 snidg 4177 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝑥) ∈ V → (𝑋𝑥) ∈ {(𝑋𝑥)})
1038, 102syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Fil‘𝑋) → (𝑋𝑥) ∈ {(𝑋𝑥)})
1041033ad2ant1 1080 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ {(𝑋𝑥)})
105104ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋𝑥) ∈ {(𝑋𝑥)})
106101, 105sseldd 3584 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋𝑥) ∈ 𝑓)
107 filin 21568 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓 ∧ (𝑋𝑥) ∈ 𝑓) → (𝑥 ∩ (𝑋𝑥)) ∈ 𝑓)
10891, 92, 106, 107syl3anc 1323 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑥 ∩ (𝑋𝑥)) ∈ 𝑓)
10990, 108syl5eqelr 2703 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → ∅ ∈ 𝑓)
110109expr 642 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑥𝑓 → ∅ ∈ 𝑓))
11189, 110mtod 189 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → ¬ 𝑥𝑓)
11285, 111jca 554 . . . . . . . . . . . . 13 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝐹𝑓 ∧ ¬ 𝑥𝑓))
113112exp31 629 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑓 ∈ (UFil‘𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → (𝐹𝑓 ∧ ¬ 𝑥𝑓))))
114113reximdvai 3009 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
11572, 114syl5 34 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
11671, 115mpd 15 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓))
1171163expia 1264 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → (𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
118 filssufil 21626 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹𝑓)
119 filelss 21566 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓) → 𝑥𝑋)
120119ex 450 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (Fil‘𝑋) → (𝑥𝑓𝑥𝑋))
12186, 120syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ (UFil‘𝑋) → (𝑥𝑓𝑥𝑋))
122121con3d 148 . . . . . . . . . . . . . 14 (𝑓 ∈ (UFil‘𝑋) → (¬ 𝑥𝑋 → ¬ 𝑥𝑓))
123122impcom 446 . . . . . . . . . . . . 13 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → ¬ 𝑥𝑓)
124123a1d 25 . . . . . . . . . . . 12 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → (𝐹𝑓 → ¬ 𝑥𝑓))
125124ancld 575 . . . . . . . . . . 11 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → (𝐹𝑓 → (𝐹𝑓 ∧ ¬ 𝑥𝑓)))
126125reximdva 3011 . . . . . . . . . 10 𝑥𝑋 → (∃𝑓 ∈ (UFil‘𝑋)𝐹𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
127118, 126syl5com 31 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
128127adantr 481 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → (¬ 𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
129117, 128pm2.61d 170 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓))
130129ex 450 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
131 rexanali 2992 . . . . . 6 (∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓) ↔ ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓))
132130, 131syl6ib 241 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓)))
133132con4d 114 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓) → 𝑥𝐹))
1342, 133syl5bi 232 . . 3 (𝐹 ∈ (Fil‘𝑋) → (𝑥 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} → 𝑥𝐹))
135134ssrdv 3589 . 2 (𝐹 ∈ (Fil‘𝑋) → {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} ⊆ 𝐹)
136 ssintub 4460 . . 3 𝐹 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓}
137136a1i 11 . 2 (𝐹 ∈ (Fil‘𝑋) → 𝐹 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓})
138135, 137eqssd 3600 1 (𝐹 ∈ (Fil‘𝑋) → {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3186  cdif 3552  cun 3553  cin 3554  wss 3555  c0 3891  𝒫 cpw 4130  {csn 4148   cint 4440  cfv 5847  (class class class)co 6604  ficfi 8260  fBascfbas 19653  filGencfg 19654  Filcfil 21559  UFilcufil 21613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-ac2 9229
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-rpss 6890  df-om 7013  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-en 7900  df-dom 7901  df-fin 7903  df-fi 8261  df-card 8709  df-ac 8883  df-cda 8934  df-fbas 19662  df-fg 19663  df-fil 21560  df-ufil 21615
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator