Metamath Proof Explorer

Theorem csdfil

Description: The set of all elements whose complement is dominated by the base set is a filter. (Contributed by Mario Carneiro, 14-Dec-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion csdfil 
|- ( ( X e. dom card /\ _om ~<_ X ) -> { x e. ~P X | ( X \ x ) ~< X } e. ( Fil ` X ) )

Proof

Step Hyp Ref Expression
1 difeq2 
 |-  ( x = y -> ( X \ x ) = ( X \ y ) )
2 1 breq1d 
 |-  ( x = y -> ( ( X \ x ) ~< X <-> ( X \ y ) ~< X ) )
3 2 elrab 
 |-  ( y e. { x e. ~P X | ( X \ x ) ~< X } <-> ( y e. ~P X /\ ( X \ y ) ~< X ) )
4 velpw 
 |-  ( y e. ~P X <-> y C_ X )
5 4 anbi1i 
 |-  ( ( y e. ~P X /\ ( X \ y ) ~< X ) <-> ( y C_ X /\ ( X \ y ) ~< X ) )
6 3 5 bitri 
 |-  ( y e. { x e. ~P X | ( X \ x ) ~< X } <-> ( y C_ X /\ ( X \ y ) ~< X ) )
7 6 a1i 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> ( y e. { x e. ~P X | ( X \ x ) ~< X } <-> ( y C_ X /\ ( X \ y ) ~< X ) ) )
8 simpl 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> X e. dom card )
9 difid 
 |-  ( X \ X ) = (/)
10 infn0 
 |-  ( _om ~<_ X -> X =/= (/) )
11 10 adantl 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> X =/= (/) )
12 0sdomg 
 |-  ( X e. dom card -> ( (/) ~< X <-> X =/= (/) ) )
13 12 adantr 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> ( (/) ~< X <-> X =/= (/) ) )
14 11 13 mpbird 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> (/) ~< X )
15 9 14 eqbrtrid 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> ( X \ X ) ~< X )
16 difeq2 
 |-  ( y = X -> ( X \ y ) = ( X \ X ) )
17 16 breq1d 
 |-  ( y = X -> ( ( X \ y ) ~< X <-> ( X \ X ) ~< X ) )
18 17 sbcieg 
 |-  ( X e. dom card -> ( [. X / y ]. ( X \ y ) ~< X <-> ( X \ X ) ~< X ) )
19 18 adantr 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> ( [. X / y ]. ( X \ y ) ~< X <-> ( X \ X ) ~< X ) )
20 15 19 mpbird 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> [. X / y ]. ( X \ y ) ~< X )
21 sdomirr 
 |-  -. X ~< X
22 0ex 
 |-  (/) e. _V
23 difeq2 
 |-  ( y = (/) -> ( X \ y ) = ( X \ (/) ) )
24 dif0 
 |-  ( X \ (/) ) = X
25 23 24 eqtrdi 
 |-  ( y = (/) -> ( X \ y ) = X )
26 25 breq1d 
 |-  ( y = (/) -> ( ( X \ y ) ~< X <-> X ~< X ) )
27 22 26 sbcie 
 |-  ( [. (/) / y ]. ( X \ y ) ~< X <-> X ~< X )
28 27 a1i 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> ( [. (/) / y ]. ( X \ y ) ~< X <-> X ~< X ) )
29 21 28 mtbiri 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> -. [. (/) / y ]. ( X \ y ) ~< X )
30 simp1l 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ z ) -> X e. dom card )
31 30 difexd 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ z ) -> ( X \ w ) e. _V )
32 sscon 
 |-  ( w C_ z -> ( X \ z ) C_ ( X \ w ) )
33 32 3ad2ant3 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ z ) -> ( X \ z ) C_ ( X \ w ) )
34 ssdomg 
 |-  ( ( X \ w ) e. _V -> ( ( X \ z ) C_ ( X \ w ) -> ( X \ z ) ~<_ ( X \ w ) ) )
35 31 33 34 sylc 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ z ) -> ( X \ z ) ~<_ ( X \ w ) )
36 domsdomtr 
 |-  ( ( ( X \ z ) ~<_ ( X \ w ) /\ ( X \ w ) ~< X ) -> ( X \ z ) ~< X )
37 36 ex 
 |-  ( ( X \ z ) ~<_ ( X \ w ) -> ( ( X \ w ) ~< X -> ( X \ z ) ~< X ) )
38 35 37 syl 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ z ) -> ( ( X \ w ) ~< X -> ( X \ z ) ~< X ) )
39 vex 
 |-  w e. _V
40 difeq2 
 |-  ( y = w -> ( X \ y ) = ( X \ w ) )
41 40 breq1d 
 |-  ( y = w -> ( ( X \ y ) ~< X <-> ( X \ w ) ~< X ) )
42 39 41 sbcie 
 |-  ( [. w / y ]. ( X \ y ) ~< X <-> ( X \ w ) ~< X )
43 vex 
 |-  z e. _V
44 difeq2 
 |-  ( y = z -> ( X \ y ) = ( X \ z ) )
45 44 breq1d 
 |-  ( y = z -> ( ( X \ y ) ~< X <-> ( X \ z ) ~< X ) )
46 43 45 sbcie 
 |-  ( [. z / y ]. ( X \ y ) ~< X <-> ( X \ z ) ~< X )
47 38 42 46 3imtr4g 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ z ) -> ( [. w / y ]. ( X \ y ) ~< X -> [. z / y ]. ( X \ y ) ~< X ) )
48 infunsdom 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( ( X \ z ) ~< X /\ ( X \ w ) ~< X ) ) -> ( ( X \ z ) u. ( X \ w ) ) ~< X )
49 48 ex 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> ( ( ( X \ z ) ~< X /\ ( X \ w ) ~< X ) -> ( ( X \ z ) u. ( X \ w ) ) ~< X ) )
50 difindi 
 |-  ( X \ ( z i^i w ) ) = ( ( X \ z ) u. ( X \ w ) )
51 50 breq1i 
 |-  ( ( X \ ( z i^i w ) ) ~< X <-> ( ( X \ z ) u. ( X \ w ) ) ~< X )
52 49 51 syl6ibr 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> ( ( ( X \ z ) ~< X /\ ( X \ w ) ~< X ) -> ( X \ ( z i^i w ) ) ~< X ) )
53 52 3ad2ant1 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ X ) -> ( ( ( X \ z ) ~< X /\ ( X \ w ) ~< X ) -> ( X \ ( z i^i w ) ) ~< X ) )
54 46 42 anbi12i 
 |-  ( ( [. z / y ]. ( X \ y ) ~< X /\ [. w / y ]. ( X \ y ) ~< X ) <-> ( ( X \ z ) ~< X /\ ( X \ w ) ~< X ) )
55 43 inex1 
 |-  ( z i^i w ) e. _V
56 difeq2 
 |-  ( y = ( z i^i w ) -> ( X \ y ) = ( X \ ( z i^i w ) ) )
57 56 breq1d 
 |-  ( y = ( z i^i w ) -> ( ( X \ y ) ~< X <-> ( X \ ( z i^i w ) ) ~< X ) )
58 55 57 sbcie 
 |-  ( [. ( z i^i w ) / y ]. ( X \ y ) ~< X <-> ( X \ ( z i^i w ) ) ~< X )
59 53 54 58 3imtr4g 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ X ) -> ( ( [. z / y ]. ( X \ y ) ~< X /\ [. w / y ]. ( X \ y ) ~< X ) -> [. ( z i^i w ) / y ]. ( X \ y ) ~< X ) )
60 7 8 20 29 47 59 isfild 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> { x e. ~P X | ( X \ x ) ~< X } e. ( Fil ` X ) )