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

Theorem filufint 22132
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 3401 . . . . 5 𝑥 ∈ V
21elintrab 4722 . . . 4 (𝑥 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} ↔ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓))
3 filsspw 22063 . . . . . . . . . . . . . 14 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
433ad2ant1 1124 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ 𝒫 𝑋)
5 difss 3960 . . . . . . . . . . . . . . 15 (𝑋𝑥) ⊆ 𝑋
6 filtop 22067 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
7 difexg 5045 . . . . . . . . . . . . . . . . . 18 (𝑋𝐹 → (𝑋𝑥) ∈ V)
86, 7syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Fil‘𝑋) → (𝑋𝑥) ∈ V)
983ad2ant1 1124 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ V)
10 elpwg 4387 . . . . . . . . . . . . . . . 16 ((𝑋𝑥) ∈ V → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
119, 10syl 17 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑋𝑥) ∈ 𝒫 𝑋 ↔ (𝑋𝑥) ⊆ 𝑋))
125, 11mpbiri 250 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ 𝒫 𝑋)
1312snssd 4571 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ⊆ 𝒫 𝑋)
144, 13unssd 4012 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋)
15 ssun1 3999 . . . . . . . . . . . . . 14 𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)})
16 filn0 22074 . . . . . . . . . . . . . 14 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
17 ssn0 4202 . . . . . . . . . . . . . 14 ((𝐹 ⊆ (𝐹 ∪ {(𝑋𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
1815, 16, 17sylancr 581 . . . . . . . . . . . . 13 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
19183ad2ant1 1124 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅)
20 elsni 4415 . . . . . . . . . . . . . . 15 (𝑧 ∈ {(𝑋𝑥)} → 𝑧 = (𝑋𝑥))
21 filelss 22064 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
22213adant3 1123 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → 𝑦𝑋)
23 reldisj 4245 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑋 → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋𝑥))))
2422, 23syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋𝑥))))
25 dfss4 4085 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝑋 ↔ (𝑋 ∖ (𝑋𝑥)) = 𝑥)
2625biimpi 208 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑋 → (𝑋 ∖ (𝑋𝑥)) = 𝑥)
2726sseq2d 3852 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝑋 → (𝑦 ⊆ (𝑋 ∖ (𝑋𝑥)) ↔ 𝑦𝑥))
28273ad2ant3 1126 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (𝑦 ⊆ (𝑋 ∖ (𝑋𝑥)) ↔ 𝑦𝑥))
2924, 28bitrd 271 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ ↔ 𝑦𝑥))
30 filss 22065 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑥𝑋𝑦𝑥)) → 𝑥𝐹)
31303exp2 1416 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → (𝑦𝐹 → (𝑥𝑋 → (𝑦𝑥𝑥𝐹))))
32313imp 1098 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (𝑦𝑥𝑥𝐹))
3329, 32sylbid 232 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → ((𝑦 ∩ (𝑋𝑥)) = ∅ → 𝑥𝐹))
3433necon3bd 2983 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹𝑥𝑋) → (¬ 𝑥𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))
35343exp 1109 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (Fil‘𝑋) → (𝑦𝐹 → (𝑥𝑋 → (¬ 𝑥𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))))
3635com24 95 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → (𝑥𝑋 → (𝑦𝐹 → (𝑦 ∩ (𝑋𝑥)) ≠ ∅))))
37363imp1 1409 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑦𝐹) → (𝑦 ∩ (𝑋𝑥)) ≠ ∅)
38 ineq2 4031 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑋𝑥) → (𝑦𝑧) = (𝑦 ∩ (𝑋𝑥)))
3938neeq1d 3028 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑋𝑥) → ((𝑦𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑋𝑥)) ≠ ∅))
4037, 39syl5ibrcom 239 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑦𝐹) → (𝑧 = (𝑋𝑥) → (𝑦𝑧) ≠ ∅))
4140expimpd 447 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑦𝐹𝑧 = (𝑋𝑥)) → (𝑦𝑧) ≠ ∅))
4220, 41sylan2i 599 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑦𝐹𝑧 ∈ {(𝑋𝑥)}) → (𝑦𝑧) ≠ ∅))
4342ralrimivv 3152 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅)
44 filfbas 22060 . . . . . . . . . . . . . . 15 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
45443ad2ant1 1124 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ∈ (fBas‘𝑋))
465a1i 11 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ⊆ 𝑋)
47263ad2ant2 1125 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → (𝑋 ∖ (𝑋𝑥)) = 𝑥)
48 difeq2 3945 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝑥) = ∅ → (𝑋 ∖ (𝑋𝑥)) = (𝑋 ∖ ∅))
49 dif0 4181 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∖ ∅) = 𝑋
5048, 49syl6eq 2830 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋𝑥) = ∅ → (𝑋 ∖ (𝑋𝑥)) = 𝑋)
51503ad2ant3 1126 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → (𝑋 ∖ (𝑋𝑥)) = 𝑋)
5247, 51eqtr3d 2816 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑥 = 𝑋)
5363ad2ant1 1124 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑋𝐹)
5452, 53eqeltrd 2859 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋 ∧ (𝑋𝑥) = ∅) → 𝑥𝐹)
55543expia 1111 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → ((𝑋𝑥) = ∅ → 𝑥𝐹))
5655necon3bd 2983 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → (¬ 𝑥𝐹 → (𝑋𝑥) ≠ ∅))
5756ex 403 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Fil‘𝑋) → (𝑥𝑋 → (¬ 𝑥𝐹 → (𝑋𝑥) ≠ ∅)))
5857com23 86 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → (𝑥𝑋 → (𝑋𝑥) ≠ ∅)))
59583imp 1098 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ≠ ∅)
6063ad2ant1 1124 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝑋𝐹)
61 snfbas 22078 . . . . . . . . . . . . . . 15 (((𝑋𝑥) ⊆ 𝑋 ∧ (𝑋𝑥) ≠ ∅ ∧ 𝑋𝐹) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
6246, 59, 60, 61syl3anc 1439 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ∈ (fBas‘𝑋))
63 fbunfip 22081 . . . . . . . . . . . . . 14 ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅))
6445, 62, 63syl2anc 579 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})) ↔ ∀𝑦𝐹𝑧 ∈ {(𝑋𝑥)} (𝑦𝑧) ≠ ∅))
6543, 64mpbird 249 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
66 fsubbas 22079 . . . . . . . . . . . . . 14 (𝑋𝐹 → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
676, 66syl 17 . . . . . . . . . . . . 13 (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
68673ad2ant1 1124 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {(𝑋𝑥)})))))
6914, 19, 65, 68mpbir3and 1399 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋))
70 fgcl 22090 . . . . . . . . . . 11 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
7169, 70syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋))
72 filssufil 22124 . . . . . . . . . . 11 ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
73 snex 5140 . . . . . . . . . . . . . . . . . . . . 21 {(𝑋𝑥)} ∈ V
74 unexg 7236 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋𝑥)} ∈ V) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
7573, 74mpan2 681 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ∈ V)
76 ssfii 8613 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∪ {(𝑋𝑥)}) ∈ V → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
7775, 76syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
78773ad2ant1 1124 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝐹 ∪ {(𝑋𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
7978unssad 4013 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
80 ssfg 22084 . . . . . . . . . . . . . . . . . 18 ((fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8169, 80syl 17 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8279, 81sstrd 3831 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
8382ad2antrr 716 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
84 simpr 479 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
8583, 84sstrd 3831 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → 𝐹𝑓)
86 ufilfil 22116 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋))
87 0nelfil 22061 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
8886, 87syl 17 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (UFil‘𝑋) → ¬ ∅ ∈ 𝑓)
8988ad2antlr 717 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → ¬ ∅ ∈ 𝑓)
90 disjdif 4264 . . . . . . . . . . . . . . . . 17 (𝑥 ∩ (𝑋𝑥)) = ∅
9186ad2antlr 717 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → 𝑓 ∈ (Fil‘𝑋))
92 simprr 763 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → 𝑥𝑓)
9377unssbd 4014 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 ∈ (Fil‘𝑋) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
94933ad2ant1 1124 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
9594adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋𝑥)})))
9669adantr 474 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ∈ (fBas‘𝑋))
9796, 80syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
9895, 97sstrd 3831 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
9998adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → {(𝑋𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))))
100 simprl 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓)
10199, 100sstrd 3831 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → {(𝑋𝑥)} ⊆ 𝑓)
102 snidg 4428 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝑥) ∈ V → (𝑋𝑥) ∈ {(𝑋𝑥)})
1038, 102syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Fil‘𝑋) → (𝑋𝑥) ∈ {(𝑋𝑥)})
1041033ad2ant1 1124 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑋𝑥) ∈ {(𝑋𝑥)})
105104ad2antrr 716 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋𝑥) ∈ {(𝑋𝑥)})
106101, 105sseldd 3822 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑋𝑥) ∈ 𝑓)
107 filin 22066 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓 ∧ (𝑋𝑥) ∈ 𝑓) → (𝑥 ∩ (𝑋𝑥)) ∈ 𝑓)
10891, 92, 106, 107syl3anc 1439 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → (𝑥 ∩ (𝑋𝑥)) ∈ 𝑓)
10990, 108syl5eqelr 2864 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓𝑥𝑓)) → ∅ ∈ 𝑓)
110109expr 450 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝑥𝑓 → ∅ ∈ 𝑓))
11189, 110mtod 190 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → ¬ 𝑥𝑓)
11285, 111jca 507 . . . . . . . . . . . . 13 ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓) → (𝐹𝑓 ∧ ¬ 𝑥𝑓))
113112exp31 412 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (𝑓 ∈ (UFil‘𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → (𝐹𝑓 ∧ ¬ 𝑥𝑓))))
114113reximdvai 3196 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → (∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
11572, 114syl5 34 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
11671, 115mpd 15 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹𝑥𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓))
1171163expia 1111 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → (𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
118 filssufil 22124 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹𝑓)
119 filelss 22064 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓) → 𝑥𝑋)
120119ex 403 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (Fil‘𝑋) → (𝑥𝑓𝑥𝑋))
12186, 120syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ (UFil‘𝑋) → (𝑥𝑓𝑥𝑋))
122121con3d 150 . . . . . . . . . . . . . 14 (𝑓 ∈ (UFil‘𝑋) → (¬ 𝑥𝑋 → ¬ 𝑥𝑓))
123122impcom 398 . . . . . . . . . . . . 13 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → ¬ 𝑥𝑓)
124123a1d 25 . . . . . . . . . . . 12 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → (𝐹𝑓 → ¬ 𝑥𝑓))
125124ancld 546 . . . . . . . . . . 11 ((¬ 𝑥𝑋𝑓 ∈ (UFil‘𝑋)) → (𝐹𝑓 → (𝐹𝑓 ∧ ¬ 𝑥𝑓)))
126125reximdva 3198 . . . . . . . . . 10 𝑥𝑋 → (∃𝑓 ∈ (UFil‘𝑋)𝐹𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
127118, 126syl5com 31 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
128127adantr 474 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → (¬ 𝑥𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
129117, 128pm2.61d 172 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥𝐹) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓))
130129ex 403 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓)))
131 rexanali 3179 . . . . . 6 (∃𝑓 ∈ (UFil‘𝑋)(𝐹𝑓 ∧ ¬ 𝑥𝑓) ↔ ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓))
132130, 131syl6ib 243 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥𝐹 → ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓)))
133132con4d 115 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹𝑓𝑥𝑓) → 𝑥𝐹))
1342, 133syl5bi 234 . . 3 (𝐹 ∈ (Fil‘𝑋) → (𝑥 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} → 𝑥𝐹))
135134ssrdv 3827 . 2 (𝐹 ∈ (Fil‘𝑋) → {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} ⊆ 𝐹)
136 ssintub 4728 . . 3 𝐹 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓}
137136a1i 11 . 2 (𝐹 ∈ (Fil‘𝑋) → 𝐹 {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓})
138135, 137eqssd 3838 1 (𝐹 ∈ (Fil‘𝑋) → {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹𝑓} = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2107  wne 2969  wral 3090  wrex 3091  {crab 3094  Vcvv 3398  cdif 3789  cun 3790  cin 3791  wss 3792  c0 4141  𝒫 cpw 4379  {csn 4398   cint 4710  cfv 6135  (class class class)co 6922  ficfi 8604  fBascfbas 20130  filGencfg 20131  Filcfil 22057  UFilcufil 22111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-ac2 9620
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-rpss 7214  df-om 7344  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-en 8242  df-dom 8243  df-fin 8245  df-fi 8605  df-card 9098  df-ac 9272  df-cda 9325  df-fbas 20139  df-fg 20140  df-fil 22058  df-ufil 22113
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator