Metamath Proof Explorer

Theorem uffixfr

Description: An ultrafilter is either fixed or free. A fixed ultrafilter is called principal (generated by a single element A ), and a free ultrafilter is called nonprincipal (having empty intersection). Note that examples of free ultrafilters cannot be defined in ZFC without some form of global choice. (Contributed by Jeff Hankins, 4-Dec-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion uffixfr 
|- ( F e. ( UFil ` X ) -> ( A e. |^| F <-> F = { x e. ~P X | A e. x } ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> F e. ( UFil ` X ) )
2 ufilfil 
 |-  ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
3 filtop 
 |-  ( F e. ( Fil ` X ) -> X e. F )
4 2 3 syl 
 |-  ( F e. ( UFil ` X ) -> X e. F )
5 filn0 
 |-  ( F e. ( Fil ` X ) -> F =/= (/) )
6 intssuni 
 |-  ( F =/= (/) -> |^| F C_ U. F )
7 2 5 6 3syl 
 |-  ( F e. ( UFil ` X ) -> |^| F C_ U. F )
8 filunibas 
 |-  ( F e. ( Fil ` X ) -> U. F = X )
9 2 8 syl 
 |-  ( F e. ( UFil ` X ) -> U. F = X )
10 7 9 sseqtrd 
 |-  ( F e. ( UFil ` X ) -> |^| F C_ X )
11 10 sselda 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> A e. X )
12 uffix 
 |-  ( ( X e. F /\ A e. X ) -> ( { { A } } e. ( fBas ` X ) /\ { x e. ~P X | A e. x } = ( X filGen { { A } } ) ) )
13 4 11 12 syl2an2r 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> ( { { A } } e. ( fBas ` X ) /\ { x e. ~P X | A e. x } = ( X filGen { { A } } ) ) )
14 13 simprd 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { x e. ~P X | A e. x } = ( X filGen { { A } } ) )
15 13 simpld 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { { A } } e. ( fBas ` X ) )
16 fgcl 
 |-  ( { { A } } e. ( fBas ` X ) -> ( X filGen { { A } } ) e. ( Fil ` X ) )
17 15 16 syl 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> ( X filGen { { A } } ) e. ( Fil ` X ) )
18 14 17 eqeltrd 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { x e. ~P X | A e. x } e. ( Fil ` X ) )
19 2 adantr 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> F e. ( Fil ` X ) )
20 filsspw 
 |-  ( F e. ( Fil ` X ) -> F C_ ~P X )
21 19 20 syl 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> F C_ ~P X )
22 elintg 
 |-  ( A e. |^| F -> ( A e. |^| F <-> A. x e. F A e. x ) )
23 22 ibi 
 |-  ( A e. |^| F -> A. x e. F A e. x )
24 23 adantl 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> A. x e. F A e. x )
25 ssrab 
 |-  ( F C_ { x e. ~P X | A e. x } <-> ( F C_ ~P X /\ A. x e. F A e. x ) )
26 21 24 25 sylanbrc 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> F C_ { x e. ~P X | A e. x } )
27 ufilmax 
 |-  ( ( F e. ( UFil ` X ) /\ { x e. ~P X | A e. x } e. ( Fil ` X ) /\ F C_ { x e. ~P X | A e. x } ) -> F = { x e. ~P X | A e. x } )
28 1 18 26 27 syl3anc 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> F = { x e. ~P X | A e. x } )
29 eqimss 
 |-  ( F = { x e. ~P X | A e. x } -> F C_ { x e. ~P X | A e. x } )
30 29 adantl 
 |-  ( ( F e. ( UFil ` X ) /\ F = { x e. ~P X | A e. x } ) -> F C_ { x e. ~P X | A e. x } )
31 25 simprbi 
 |-  ( F C_ { x e. ~P X | A e. x } -> A. x e. F A e. x )
32 30 31 syl 
 |-  ( ( F e. ( UFil ` X ) /\ F = { x e. ~P X | A e. x } ) -> A. x e. F A e. x )
33 eleq2 
 |-  ( F = { x e. ~P X | A e. x } -> ( X e. F <-> X e. { x e. ~P X | A e. x } ) )
34 33 biimpac 
 |-  ( ( X e. F /\ F = { x e. ~P X | A e. x } ) -> X e. { x e. ~P X | A e. x } )
35 4 34 sylan 
 |-  ( ( F e. ( UFil ` X ) /\ F = { x e. ~P X | A e. x } ) -> X e. { x e. ~P X | A e. x } )
36 eleq2 
 |-  ( x = X -> ( A e. x <-> A e. X ) )
37 36 elrab 
 |-  ( X e. { x e. ~P X | A e. x } <-> ( X e. ~P X /\ A e. X ) )
38 37 simprbi 
 |-  ( X e. { x e. ~P X | A e. x } -> A e. X )
39 elintg 
 |-  ( A e. X -> ( A e. |^| F <-> A. x e. F A e. x ) )
40 35 38 39 3syl 
 |-  ( ( F e. ( UFil ` X ) /\ F = { x e. ~P X | A e. x } ) -> ( A e. |^| F <-> A. x e. F A e. x ) )
41 32 40 mpbird 
 |-  ( ( F e. ( UFil ` X ) /\ F = { x e. ~P X | A e. x } ) -> A e. |^| F )
42 28 41 impbida 
 |-  ( F e. ( UFil ` X ) -> ( A e. |^| F <-> F = { x e. ~P X | A e. x } ) )