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 e. V /\ A e. X ) -> { x e. ~P X | A e. x } e. ( UFil ` X ) )

Proof

Step Hyp Ref Expression
1 uffix 
 |-  ( ( X e. V /\ A e. X ) -> ( { { A } } e. ( fBas ` X ) /\ { x e. ~P X | A e. x } = ( X filGen { { A } } ) ) )
2 1 simprd 
 |-  ( ( X e. V /\ A e. X ) -> { x e. ~P X | A e. x } = ( X filGen { { A } } ) )
3 1 simpld 
 |-  ( ( X e. V /\ A e. X ) -> { { A } } e. ( fBas ` X ) )
4 fgcl 
 |-  ( { { A } } e. ( fBas ` X ) -> ( X filGen { { A } } ) e. ( Fil ` X ) )
5 3 4 syl 
 |-  ( ( X e. V /\ A e. X ) -> ( X filGen { { A } } ) e. ( Fil ` X ) )
6 2 5 eqeltrd 
 |-  ( ( X e. V /\ A e. X ) -> { x e. ~P X | A e. x } e. ( Fil ` X ) )
7 undif2 
 |-  ( y u. ( X \ y ) ) = ( y u. X )
8 elpwi 
 |-  ( y e. ~P X -> y C_ X )
9 ssequn1 
 |-  ( y C_ X <-> ( y u. X ) = X )
10 8 9 sylib 
 |-  ( y e. ~P X -> ( y u. X ) = X )
11 7 10 syl5req 
 |-  ( y e. ~P X -> X = ( y u. ( X \ y ) ) )
12 11 eleq2d 
 |-  ( y e. ~P X -> ( A e. X <-> A e. ( y u. ( X \ y ) ) ) )
13 12 biimpac 
 |-  ( ( A e. X /\ y e. ~P X ) -> A e. ( y u. ( X \ y ) ) )
14 elun 
 |-  ( A e. ( y u. ( X \ y ) ) <-> ( A e. y \/ A e. ( X \ y ) ) )
15 13 14 sylib 
 |-  ( ( A e. X /\ y e. ~P X ) -> ( A e. y \/ A e. ( X \ y ) ) )
16 15 adantll 
 |-  ( ( ( X e. V /\ A e. X ) /\ y e. ~P X ) -> ( A e. y \/ A e. ( X \ y ) ) )
17 ibar 
 |-  ( y e. ~P X -> ( A e. y <-> ( y e. ~P X /\ A e. y ) ) )
18 17 adantl 
 |-  ( ( ( X e. V /\ A e. X ) /\ y e. ~P X ) -> ( A e. y <-> ( y e. ~P X /\ A e. y ) ) )
19 difss 
 |-  ( X \ y ) C_ X
20 elpw2g 
 |-  ( X e. V -> ( ( X \ y ) e. ~P X <-> ( X \ y ) C_ X ) )
21 19 20 mpbiri 
 |-  ( X e. V -> ( X \ y ) e. ~P X )
22 21 ad2antrr 
 |-  ( ( ( X e. V /\ A e. X ) /\ y e. ~P X ) -> ( X \ y ) e. ~P X )
23 22 biantrurd 
 |-  ( ( ( X e. V /\ A e. X ) /\ y e. ~P X ) -> ( A e. ( X \ y ) <-> ( ( X \ y ) e. ~P X /\ A e. ( X \ y ) ) ) )
24 18 23 orbi12d 
 |-  ( ( ( X e. V /\ A e. X ) /\ y e. ~P X ) -> ( ( A e. y \/ A e. ( X \ y ) ) <-> ( ( y e. ~P X /\ A e. y ) \/ ( ( X \ y ) e. ~P X /\ A e. ( X \ y ) ) ) ) )
25 16 24 mpbid 
 |-  ( ( ( X e. V /\ A e. X ) /\ y e. ~P X ) -> ( ( y e. ~P X /\ A e. y ) \/ ( ( X \ y ) e. ~P X /\ A e. ( X \ y ) ) ) )
26 25 ralrimiva 
 |-  ( ( X e. V /\ A e. X ) -> A. y e. ~P X ( ( y e. ~P X /\ A e. y ) \/ ( ( X \ y ) e. ~P X /\ A e. ( X \ y ) ) ) )
27 eleq2 
 |-  ( x = y -> ( A e. x <-> A e. y ) )
28 27 elrab 
 |-  ( y e. { x e. ~P X | A e. x } <-> ( y e. ~P X /\ A e. y ) )
29 eleq2 
 |-  ( x = ( X \ y ) -> ( A e. x <-> A e. ( X \ y ) ) )
30 29 elrab 
 |-  ( ( X \ y ) e. { x e. ~P X | A e. x } <-> ( ( X \ y ) e. ~P X /\ A e. ( X \ y ) ) )
31 28 30 orbi12i 
 |-  ( ( y e. { x e. ~P X | A e. x } \/ ( X \ y ) e. { x e. ~P X | A e. x } ) <-> ( ( y e. ~P X /\ A e. y ) \/ ( ( X \ y ) e. ~P X /\ A e. ( X \ y ) ) ) )
32 31 ralbii 
 |-  ( A. y e. ~P X ( y e. { x e. ~P X | A e. x } \/ ( X \ y ) e. { x e. ~P X | A e. x } ) <-> A. y e. ~P X ( ( y e. ~P X /\ A e. y ) \/ ( ( X \ y ) e. ~P X /\ A e. ( X \ y ) ) ) )
33 26 32 sylibr 
 |-  ( ( X e. V /\ A e. X ) -> A. y e. ~P X ( y e. { x e. ~P X | A e. x } \/ ( X \ y ) e. { x e. ~P X | A e. x } ) )
34 isufil 
 |-  ( { x e. ~P X | A e. x } e. ( UFil ` X ) <-> ( { x e. ~P X | A e. x } e. ( Fil ` X ) /\ A. y e. ~P X ( y e. { x e. ~P X | A e. x } \/ ( X \ y ) e. { x e. ~P X | A e. x } ) ) )
35 6 33 34 sylanbrc 
 |-  ( ( X e. V /\ A e. X ) -> { x e. ~P X | A e. x } e. ( UFil ` X ) )