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 difexg 
 |-  ( X e. dom card -> ( X \ w ) e. _V )
32 30 31 syl 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ z ) -> ( X \ w ) e. _V )
33 sscon 
 |-  ( w C_ z -> ( X \ z ) C_ ( X \ w ) )
34 33 3ad2ant3 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ z ) -> ( X \ z ) C_ ( X \ w ) )
35 ssdomg 
 |-  ( ( X \ w ) e. _V -> ( ( X \ z ) C_ ( X \ w ) -> ( X \ z ) ~<_ ( X \ w ) ) )
36 32 34 35 sylc 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ z ) -> ( X \ z ) ~<_ ( X \ w ) )
37 domsdomtr 
 |-  ( ( ( X \ z ) ~<_ ( X \ w ) /\ ( X \ w ) ~< X ) -> ( X \ z ) ~< X )
38 37 ex 
 |-  ( ( X \ z ) ~<_ ( X \ w ) -> ( ( X \ w ) ~< X -> ( X \ z ) ~< X ) )
39 36 38 syl 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ z ) -> ( ( X \ w ) ~< X -> ( X \ z ) ~< X ) )
40 vex 
 |-  w e. _V
41 difeq2 
 |-  ( y = w -> ( X \ y ) = ( X \ w ) )
42 41 breq1d 
 |-  ( y = w -> ( ( X \ y ) ~< X <-> ( X \ w ) ~< X ) )
43 40 42 sbcie 
 |-  ( [. w / y ]. ( X \ y ) ~< X <-> ( X \ w ) ~< X )
44 vex 
 |-  z e. _V
45 difeq2 
 |-  ( y = z -> ( X \ y ) = ( X \ z ) )
46 45 breq1d 
 |-  ( y = z -> ( ( X \ y ) ~< X <-> ( X \ z ) ~< X ) )
47 44 46 sbcie 
 |-  ( [. z / y ]. ( X \ y ) ~< X <-> ( X \ z ) ~< X )
48 39 43 47 3imtr4g 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ z C_ X /\ w C_ z ) -> ( [. w / y ]. ( X \ y ) ~< X -> [. z / y ]. ( X \ y ) ~< X ) )
49 infunsdom 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( ( X \ z ) ~< X /\ ( X \ w ) ~< X ) ) -> ( ( X \ z ) u. ( X \ w ) ) ~< X )
50 49 ex 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> ( ( ( X \ z ) ~< X /\ ( X \ w ) ~< X ) -> ( ( X \ z ) u. ( X \ w ) ) ~< X ) )
51 difindi 
 |-  ( X \ ( z i^i w ) ) = ( ( X \ z ) u. ( X \ w ) )
52 51 breq1i 
 |-  ( ( X \ ( z i^i w ) ) ~< X <-> ( ( X \ z ) u. ( X \ w ) ) ~< X )
53 50 52 syl6ibr 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> ( ( ( X \ z ) ~< X /\ ( X \ w ) ~< X ) -> ( X \ ( z i^i w ) ) ~< X ) )
54 53 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 ) )
55 47 43 anbi12i 
 |-  ( ( [. z / y ]. ( X \ y ) ~< X /\ [. w / y ]. ( X \ y ) ~< X ) <-> ( ( X \ z ) ~< X /\ ( X \ w ) ~< X ) )
56 44 inex1 
 |-  ( z i^i w ) e. _V
57 difeq2 
 |-  ( y = ( z i^i w ) -> ( X \ y ) = ( X \ ( z i^i w ) ) )
58 57 breq1d 
 |-  ( y = ( z i^i w ) -> ( ( X \ y ) ~< X <-> ( X \ ( z i^i w ) ) ~< X ) )
59 56 58 sbcie 
 |-  ( [. ( z i^i w ) / y ]. ( X \ y ) ~< X <-> ( X \ ( z i^i w ) ) ~< X )
60 54 55 59 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 ) )
61 7 8 20 29 48 60 isfild 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> { x e. ~P X | ( X \ x ) ~< X } e. ( Fil ` X ) )