Metamath Proof Explorer

Theorem cfinufil

Description: An ultrafilter is free iff it contains the Fréchet filter cfinfil as a subset. (Contributed by NM, 14-Jul-2008) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion cfinufil 
|- ( F e. ( UFil ` X ) -> ( |^| F = (/) <-> { x e. ~P X | ( X \ x ) e. Fin } C_ F ) )

Proof

Step Hyp Ref Expression
1 elpwi 
 |-  ( x e. ~P X -> x C_ X )
2 ufilb 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( -. x e. F <-> ( X \ x ) e. F ) )
3 2 adantr 
 |-  ( ( ( F e. ( UFil ` X ) /\ x C_ X ) /\ ( X \ x ) e. Fin ) -> ( -. x e. F <-> ( X \ x ) e. F ) )
4 ufilfil 
 |-  ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
5 4 adantr 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> F e. ( Fil ` X ) )
6 filfinnfr 
 |-  ( ( F e. ( Fil ` X ) /\ ( X \ x ) e. F /\ ( X \ x ) e. Fin ) -> |^| F =/= (/) )
7 6 3exp 
 |-  ( F e. ( Fil ` X ) -> ( ( X \ x ) e. F -> ( ( X \ x ) e. Fin -> |^| F =/= (/) ) ) )
8 7 com23 
 |-  ( F e. ( Fil ` X ) -> ( ( X \ x ) e. Fin -> ( ( X \ x ) e. F -> |^| F =/= (/) ) ) )
9 5 8 syl 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( ( X \ x ) e. Fin -> ( ( X \ x ) e. F -> |^| F =/= (/) ) ) )
10 9 imp 
 |-  ( ( ( F e. ( UFil ` X ) /\ x C_ X ) /\ ( X \ x ) e. Fin ) -> ( ( X \ x ) e. F -> |^| F =/= (/) ) )
11 3 10 sylbid 
 |-  ( ( ( F e. ( UFil ` X ) /\ x C_ X ) /\ ( X \ x ) e. Fin ) -> ( -. x e. F -> |^| F =/= (/) ) )
12 11 necon4bd 
 |-  ( ( ( F e. ( UFil ` X ) /\ x C_ X ) /\ ( X \ x ) e. Fin ) -> ( |^| F = (/) -> x e. F ) )
13 12 ex 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( ( X \ x ) e. Fin -> ( |^| F = (/) -> x e. F ) ) )
14 13 com23 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( |^| F = (/) -> ( ( X \ x ) e. Fin -> x e. F ) ) )
15 1 14 sylan2 
 |-  ( ( F e. ( UFil ` X ) /\ x e. ~P X ) -> ( |^| F = (/) -> ( ( X \ x ) e. Fin -> x e. F ) ) )
16 15 ralrimdva 
 |-  ( F e. ( UFil ` X ) -> ( |^| F = (/) -> A. x e. ~P X ( ( X \ x ) e. Fin -> x e. F ) ) )
17 4 adantr 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> F e. ( Fil ` X ) )
18 uffixsn 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> { y } e. F )
19 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ { y } e. F ) -> { y } C_ X )
20 17 18 19 syl2anc 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> { y } C_ X )
21 dfss4 
 |-  ( { y } C_ X <-> ( X \ ( X \ { y } ) ) = { y } )
22 20 21 sylib 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> ( X \ ( X \ { y } ) ) = { y } )
23 snfi 
 |-  { y } e. Fin
24 22 23 eqeltrdi 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> ( X \ ( X \ { y } ) ) e. Fin )
25 difss 
 |-  ( X \ { y } ) C_ X
26 filtop 
 |-  ( F e. ( Fil ` X ) -> X e. F )
27 elpw2g 
 |-  ( X e. F -> ( ( X \ { y } ) e. ~P X <-> ( X \ { y } ) C_ X ) )
28 17 26 27 3syl 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> ( ( X \ { y } ) e. ~P X <-> ( X \ { y } ) C_ X ) )
29 25 28 mpbiri 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> ( X \ { y } ) e. ~P X )
30 difeq2 
 |-  ( x = ( X \ { y } ) -> ( X \ x ) = ( X \ ( X \ { y } ) ) )
31 30 eleq1d 
 |-  ( x = ( X \ { y } ) -> ( ( X \ x ) e. Fin <-> ( X \ ( X \ { y } ) ) e. Fin ) )
32 eleq1 
 |-  ( x = ( X \ { y } ) -> ( x e. F <-> ( X \ { y } ) e. F ) )
33 31 32 imbi12d 
 |-  ( x = ( X \ { y } ) -> ( ( ( X \ x ) e. Fin -> x e. F ) <-> ( ( X \ ( X \ { y } ) ) e. Fin -> ( X \ { y } ) e. F ) ) )
34 33 rspcv 
 |-  ( ( X \ { y } ) e. ~P X -> ( A. x e. ~P X ( ( X \ x ) e. Fin -> x e. F ) -> ( ( X \ ( X \ { y } ) ) e. Fin -> ( X \ { y } ) e. F ) ) )
35 29 34 syl 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> ( A. x e. ~P X ( ( X \ x ) e. Fin -> x e. F ) -> ( ( X \ ( X \ { y } ) ) e. Fin -> ( X \ { y } ) e. F ) ) )
36 24 35 mpid 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> ( A. x e. ~P X ( ( X \ x ) e. Fin -> x e. F ) -> ( X \ { y } ) e. F ) )
37 ufilb 
 |-  ( ( F e. ( UFil ` X ) /\ { y } C_ X ) -> ( -. { y } e. F <-> ( X \ { y } ) e. F ) )
38 20 37 syldan 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> ( -. { y } e. F <-> ( X \ { y } ) e. F ) )
39 18 pm2.24d 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> ( -. { y } e. F -> -. y e. |^| F ) )
40 38 39 sylbird 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> ( ( X \ { y } ) e. F -> -. y e. |^| F ) )
41 36 40 syld 
 |-  ( ( F e. ( UFil ` X ) /\ y e. |^| F ) -> ( A. x e. ~P X ( ( X \ x ) e. Fin -> x e. F ) -> -. y e. |^| F ) )
42 41 impancom 
 |-  ( ( F e. ( UFil ` X ) /\ A. x e. ~P X ( ( X \ x ) e. Fin -> x e. F ) ) -> ( y e. |^| F -> -. y e. |^| F ) )
43 42 pm2.01d 
 |-  ( ( F e. ( UFil ` X ) /\ A. x e. ~P X ( ( X \ x ) e. Fin -> x e. F ) ) -> -. y e. |^| F )
44 43 eq0rdv 
 |-  ( ( F e. ( UFil ` X ) /\ A. x e. ~P X ( ( X \ x ) e. Fin -> x e. F ) ) -> |^| F = (/) )
45 44 ex 
 |-  ( F e. ( UFil ` X ) -> ( A. x e. ~P X ( ( X \ x ) e. Fin -> x e. F ) -> |^| F = (/) ) )
46 16 45 impbid 
 |-  ( F e. ( UFil ` X ) -> ( |^| F = (/) <-> A. x e. ~P X ( ( X \ x ) e. Fin -> x e. F ) ) )
47 rabss 
 |-  ( { x e. ~P X | ( X \ x ) e. Fin } C_ F <-> A. x e. ~P X ( ( X \ x ) e. Fin -> x e. F ) )
48 46 47 bitr4di 
 |-  ( F e. ( UFil ` X ) -> ( |^| F = (/) <-> { x e. ~P X | ( X \ x ) e. Fin } C_ F ) )