Metamath Proof Explorer

Theorem fixufil

Description: The condition describing a fixed ultrafilter always produces an ultrafilter. (Contributed by Jeff Hankins, 9-Dec-2009) (Revised by Mario Carneiro, 12-Dec-2013) (Revised by Stefan O'Rear, 29-Jul-2015)

Ref Expression
Assertion fixufil ⊢X∈V∧A∈X→x∈𝒫X|A∈x∈UFil⁡X

Proof

Step Hyp Ref Expression
1 uffix ⊢X∈V∧A∈X→A∈fBas⁡X∧x∈𝒫X|A∈x=XfilGenA
2 1 simprd ⊢X∈V∧A∈X→x∈𝒫X|A∈x=XfilGenA
3 1 simpld ⊢X∈V∧A∈X→A∈fBas⁡X
4 fgcl ⊢A∈fBas⁡X→XfilGenA∈Fil⁡X
5 3 4 syl ⊢X∈V∧A∈X→XfilGenA∈Fil⁡X
6 2 5 eqeltrd ⊢X∈V∧A∈X→x∈𝒫X|A∈x∈Fil⁡X
7 undif2 ⊢y∪X∖y=y∪X
8 elpwi ⊢y∈𝒫X→y⊆X
9 ssequn1 ⊢y⊆X↔y∪X=X
10 8 9 sylib ⊢y∈𝒫X→y∪X=X
11 7 10 eqtr2id ⊢y∈𝒫X→X=y∪X∖y
12 11 eleq2d ⊢y∈𝒫X→A∈X↔A∈y∪X∖y
13 12 biimpac ⊢A∈X∧y∈𝒫X→A∈y∪X∖y
14 elun ⊢A∈y∪X∖y↔A∈y∨A∈X∖y
15 13 14 sylib ⊢A∈X∧y∈𝒫X→A∈y∨A∈X∖y
16 15 adantll ⊢X∈V∧A∈X∧y∈𝒫X→A∈y∨A∈X∖y
17 ibar ⊢y∈𝒫X→A∈y↔y∈𝒫X∧A∈y
18 17 adantl ⊢X∈V∧A∈X∧y∈𝒫X→A∈y↔y∈𝒫X∧A∈y
19 difss ⊢X∖y⊆X
20 elpw2g ⊢X∈V→X∖y∈𝒫X↔X∖y⊆X
21 19 20 mpbiri ⊢X∈V→X∖y∈𝒫X
22 21 ad2antrr ⊢X∈V∧A∈X∧y∈𝒫X→X∖y∈𝒫X
23 22 biantrurd ⊢X∈V∧A∈X∧y∈𝒫X→A∈X∖y↔X∖y∈𝒫X∧A∈X∖y
24 18 23 orbi12d ⊢X∈V∧A∈X∧y∈𝒫X→A∈y∨A∈X∖y↔y∈𝒫X∧A∈y∨X∖y∈𝒫X∧A∈X∖y
25 16 24 mpbid ⊢X∈V∧A∈X∧y∈𝒫X→y∈𝒫X∧A∈y∨X∖y∈𝒫X∧A∈X∖y
26 25 ralrimiva ⊢X∈V∧A∈X→∀y∈𝒫Xy∈𝒫X∧A∈y∨X∖y∈𝒫X∧A∈X∖y
27 eleq2 ⊢x=y→A∈x↔A∈y
28 27 elrab ⊢y∈x∈𝒫X|A∈x↔y∈𝒫X∧A∈y
29 eleq2 ⊢x=X∖y→A∈x↔A∈X∖y
30 29 elrab ⊢X∖y∈x∈𝒫X|A∈x↔X∖y∈𝒫X∧A∈X∖y
31 28 30 orbi12i ⊢y∈x∈𝒫X|A∈x∨X∖y∈x∈𝒫X|A∈x↔y∈𝒫X∧A∈y∨X∖y∈𝒫X∧A∈X∖y
32 31 ralbii ⊢∀y∈𝒫Xy∈x∈𝒫X|A∈x∨X∖y∈x∈𝒫X|A∈x↔∀y∈𝒫Xy∈𝒫X∧A∈y∨X∖y∈𝒫X∧A∈X∖y
33 26 32 sylibr ⊢X∈V∧A∈X→∀y∈𝒫Xy∈x∈𝒫X|A∈x∨X∖y∈x∈𝒫X|A∈x
34 isufil ⊢x∈𝒫X|A∈x∈UFil⁡X↔x∈𝒫X|A∈x∈Fil⁡X∧∀y∈𝒫Xy∈x∈𝒫X|A∈x∨X∖y∈x∈𝒫X|A∈x
35 6 33 34 sylanbrc ⊢X∈V∧A∈X→x∈𝒫X|A∈x∈UFil⁡X