Metamath Proof Explorer

Theorem ufinffr

Description: An infinite subset is contained in a free ultrafilter. (Contributed by Jeff Hankins, 6-Dec-2009) (Revised by Mario Carneiro, 4-Dec-2013)

Ref Expression
Assertion ufinffr 
|- ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> E. f e. ( UFil ` X ) ( A e. f /\ |^| f = (/) ) )

Proof

Step Hyp Ref Expression
1 ominf 
 |-  -. _om e. Fin
2 domfi 
 |-  ( ( A e. Fin /\ _om ~<_ A ) -> _om e. Fin )
3 2 expcom 
 |-  ( _om ~<_ A -> ( A e. Fin -> _om e. Fin ) )
4 1 3 mtoi 
 |-  ( _om ~<_ A -> -. A e. Fin )
5 cfinfil 
 |-  ( ( X e. B /\ A C_ X /\ -. A e. Fin ) -> { x e. ~P X | ( A \ x ) e. Fin } e. ( Fil ` X ) )
6 4 5 syl3an3 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> { x e. ~P X | ( A \ x ) e. Fin } e. ( Fil ` X ) )
7 filssufil 
 |-  ( { x e. ~P X | ( A \ x ) e. Fin } e. ( Fil ` X ) -> E. f e. ( UFil ` X ) { x e. ~P X | ( A \ x ) e. Fin } C_ f )
8 6 7 syl 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> E. f e. ( UFil ` X ) { x e. ~P X | ( A \ x ) e. Fin } C_ f )
9 difeq2 
 |-  ( x = A -> ( A \ x ) = ( A \ A ) )
10 difid 
 |-  ( A \ A ) = (/)
11 9 10 eqtrdi 
 |-  ( x = A -> ( A \ x ) = (/) )
12 11 eleq1d 
 |-  ( x = A -> ( ( A \ x ) e. Fin <-> (/) e. Fin ) )
13 elpw2g 
 |-  ( X e. B -> ( A e. ~P X <-> A C_ X ) )
14 13 biimpar 
 |-  ( ( X e. B /\ A C_ X ) -> A e. ~P X )
15 14 3adant3 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> A e. ~P X )
16 0fin 
 |-  (/) e. Fin
17 16 a1i 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> (/) e. Fin )
18 12 15 17 elrabd 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> A e. { x e. ~P X | ( A \ x ) e. Fin } )
19 ssel 
 |-  ( { x e. ~P X | ( A \ x ) e. Fin } C_ f -> ( A e. { x e. ~P X | ( A \ x ) e. Fin } -> A e. f ) )
20 18 19 syl5com 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> ( { x e. ~P X | ( A \ x ) e. Fin } C_ f -> A e. f ) )
21 intss 
 |-  ( { x e. ~P X | ( A \ x ) e. Fin } C_ f -> |^| f C_ |^| { x e. ~P X | ( A \ x ) e. Fin } )
22 neldifsn 
 |-  -. y e. ( A \ { y } )
23 elinti 
 |-  ( y e. |^| { x e. ~P X | ( A \ x ) e. Fin } -> ( ( A \ { y } ) e. { x e. ~P X | ( A \ x ) e. Fin } -> y e. ( A \ { y } ) ) )
24 22 23 mtoi 
 |-  ( y e. |^| { x e. ~P X | ( A \ x ) e. Fin } -> -. ( A \ { y } ) e. { x e. ~P X | ( A \ x ) e. Fin } )
25 difeq2 
 |-  ( x = ( A \ { y } ) -> ( A \ x ) = ( A \ ( A \ { y } ) ) )
26 25 eleq1d 
 |-  ( x = ( A \ { y } ) -> ( ( A \ x ) e. Fin <-> ( A \ ( A \ { y } ) ) e. Fin ) )
27 simp2 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> A C_ X )
28 27 ssdifssd 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> ( A \ { y } ) C_ X )
29 elpw2g 
 |-  ( X e. B -> ( ( A \ { y } ) e. ~P X <-> ( A \ { y } ) C_ X ) )
30 29 3ad2ant1 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> ( ( A \ { y } ) e. ~P X <-> ( A \ { y } ) C_ X ) )
31 28 30 mpbird 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> ( A \ { y } ) e. ~P X )
32 snfi 
 |-  { y } e. Fin
33 eldif 
 |-  ( x e. ( A \ ( A \ { y } ) ) <-> ( x e. A /\ -. x e. ( A \ { y } ) ) )
34 eldif 
 |-  ( x e. ( A \ { y } ) <-> ( x e. A /\ -. x e. { y } ) )
35 34 notbii 
 |-  ( -. x e. ( A \ { y } ) <-> -. ( x e. A /\ -. x e. { y } ) )
36 iman 
 |-  ( ( x e. A -> x e. { y } ) <-> -. ( x e. A /\ -. x e. { y } ) )
37 35 36 bitr4i 
 |-  ( -. x e. ( A \ { y } ) <-> ( x e. A -> x e. { y } ) )
38 37 anbi2i 
 |-  ( ( x e. A /\ -. x e. ( A \ { y } ) ) <-> ( x e. A /\ ( x e. A -> x e. { y } ) ) )
39 33 38 bitri 
 |-  ( x e. ( A \ ( A \ { y } ) ) <-> ( x e. A /\ ( x e. A -> x e. { y } ) ) )
40 pm3.35 
 |-  ( ( x e. A /\ ( x e. A -> x e. { y } ) ) -> x e. { y } )
41 39 40 sylbi 
 |-  ( x e. ( A \ ( A \ { y } ) ) -> x e. { y } )
42 41 ssriv 
 |-  ( A \ ( A \ { y } ) ) C_ { y }
43 ssfi 
 |-  ( ( { y } e. Fin /\ ( A \ ( A \ { y } ) ) C_ { y } ) -> ( A \ ( A \ { y } ) ) e. Fin )
44 32 42 43 mp2an 
 |-  ( A \ ( A \ { y } ) ) e. Fin
45 44 a1i 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> ( A \ ( A \ { y } ) ) e. Fin )
46 26 31 45 elrabd 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> ( A \ { y } ) e. { x e. ~P X | ( A \ x ) e. Fin } )
47 24 46 nsyl3 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> -. y e. |^| { x e. ~P X | ( A \ x ) e. Fin } )
48 47 eq0rdv 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> |^| { x e. ~P X | ( A \ x ) e. Fin } = (/) )
49 48 sseq2d 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> ( |^| f C_ |^| { x e. ~P X | ( A \ x ) e. Fin } <-> |^| f C_ (/) ) )
50 21 49 syl5ib 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> ( { x e. ~P X | ( A \ x ) e. Fin } C_ f -> |^| f C_ (/) ) )
51 ss0 
 |-  ( |^| f C_ (/) -> |^| f = (/) )
52 50 51 syl6 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> ( { x e. ~P X | ( A \ x ) e. Fin } C_ f -> |^| f = (/) ) )
53 20 52 jcad 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> ( { x e. ~P X | ( A \ x ) e. Fin } C_ f -> ( A e. f /\ |^| f = (/) ) ) )
54 53 reximdv 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> ( E. f e. ( UFil ` X ) { x e. ~P X | ( A \ x ) e. Fin } C_ f -> E. f e. ( UFil ` X ) ( A e. f /\ |^| f = (/) ) ) )
55 8 54 mpd 
 |-  ( ( X e. B /\ A C_ X /\ _om ~<_ A ) -> E. f e. ( UFil ` X ) ( A e. f /\ |^| f = (/) ) )