Metamath Proof Explorer

Theorem clsk1indlem1

Description: The ansatz closure function ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) does not have the K1 property of isotony. (Contributed by RP, 6-Jul-2021)

Ref Expression
Hypothesis clsk1indlem.k 
|- K = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) )
Assertion clsk1indlem1 
|- E. s e. ~P 3o E. t e. ~P 3o ( s C_ t /\ -. ( K ` s ) C_ ( K ` t ) )

Proof

Step Hyp Ref Expression
1 clsk1indlem.k 
 |-  K = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) )
2 tpex 
 |-  { (/) , 1o , 2o } e. _V
3 snsstp1 
 |-  { (/) } C_ { (/) , 1o , 2o }
4 2 3 elpwi2 
 |-  { (/) } e. ~P { (/) , 1o , 2o }
5 df3o2 
 |-  3o = { (/) , 1o , 2o }
6 5 pweqi 
 |-  ~P 3o = ~P { (/) , 1o , 2o }
7 4 6 eleqtrri 
 |-  { (/) } e. ~P 3o
8 2 a1i 
 |-  ( T. -> { (/) , 1o , 2o } e. _V )
9 3 a1i 
 |-  ( T. -> { (/) } C_ { (/) , 1o , 2o } )
10 0ex 
 |-  (/) e. _V
11 10 snss 
 |-  ( (/) e. { (/) , 1o , 2o } <-> { (/) } C_ { (/) , 1o , 2o } )
12 9 11 sylibr 
 |-  ( T. -> (/) e. { (/) , 1o , 2o } )
13 snsstp3 
 |-  { 2o } C_ { (/) , 1o , 2o }
14 13 a1i 
 |-  ( T. -> { 2o } C_ { (/) , 1o , 2o } )
15 2oex 
 |-  2o e. _V
16 15 snss 
 |-  ( 2o e. { (/) , 1o , 2o } <-> { 2o } C_ { (/) , 1o , 2o } )
17 14 16 sylibr 
 |-  ( T. -> 2o e. { (/) , 1o , 2o } )
18 12 17 prssd 
 |-  ( T. -> { (/) , 2o } C_ { (/) , 1o , 2o } )
19 8 18 sselpwd 
 |-  ( T. -> { (/) , 2o } e. ~P { (/) , 1o , 2o } )
20 19 mptru 
 |-  { (/) , 2o } e. ~P { (/) , 1o , 2o }
21 20 6 eleqtrri 
 |-  { (/) , 2o } e. ~P 3o
22 simpl 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> { (/) } e. ~P 3o )
23 sseq1 
 |-  ( s = { (/) } -> ( s C_ t <-> { (/) } C_ t ) )
24 fveq2 
 |-  ( s = { (/) } -> ( K ` s ) = ( K ` { (/) } ) )
25 24 sseq1d 
 |-  ( s = { (/) } -> ( ( K ` s ) C_ ( K ` t ) <-> ( K ` { (/) } ) C_ ( K ` t ) ) )
26 25 notbid 
 |-  ( s = { (/) } -> ( -. ( K ` s ) C_ ( K ` t ) <-> -. ( K ` { (/) } ) C_ ( K ` t ) ) )
27 23 26 anbi12d 
 |-  ( s = { (/) } -> ( ( s C_ t /\ -. ( K ` s ) C_ ( K ` t ) ) <-> ( { (/) } C_ t /\ -. ( K ` { (/) } ) C_ ( K ` t ) ) ) )
28 27 rexbidv 
 |-  ( s = { (/) } -> ( E. t e. ~P 3o ( s C_ t /\ -. ( K ` s ) C_ ( K ` t ) ) <-> E. t e. ~P 3o ( { (/) } C_ t /\ -. ( K ` { (/) } ) C_ ( K ` t ) ) ) )
29 28 adantl 
 |-  ( ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) /\ s = { (/) } ) -> ( E. t e. ~P 3o ( s C_ t /\ -. ( K ` s ) C_ ( K ` t ) ) <-> E. t e. ~P 3o ( { (/) } C_ t /\ -. ( K ` { (/) } ) C_ ( K ` t ) ) ) )
30 simpr 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> { (/) , 2o } e. ~P 3o )
31 fveq2 
 |-  ( t = { (/) , 2o } -> ( K ` t ) = ( K ` { (/) , 2o } ) )
32 31 sseq2d 
 |-  ( t = { (/) , 2o } -> ( ( K ` { (/) } ) C_ ( K ` t ) <-> ( K ` { (/) } ) C_ ( K ` { (/) , 2o } ) ) )
33 32 notbid 
 |-  ( t = { (/) , 2o } -> ( -. ( K ` { (/) } ) C_ ( K ` t ) <-> -. ( K ` { (/) } ) C_ ( K ` { (/) , 2o } ) ) )
34 33 cleq2lem 
 |-  ( t = { (/) , 2o } -> ( ( { (/) } C_ t /\ -. ( K ` { (/) } ) C_ ( K ` t ) ) <-> ( { (/) } C_ { (/) , 2o } /\ -. ( K ` { (/) } ) C_ ( K ` { (/) , 2o } ) ) ) )
35 34 adantl 
 |-  ( ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) /\ t = { (/) , 2o } ) -> ( ( { (/) } C_ t /\ -. ( K ` { (/) } ) C_ ( K ` t ) ) <-> ( { (/) } C_ { (/) , 2o } /\ -. ( K ` { (/) } ) C_ ( K ` { (/) , 2o } ) ) ) )
36 1oex 
 |-  1o e. _V
37 36 prid2 
 |-  1o e. { (/) , 1o }
38 iftrue 
 |-  ( r = { (/) } -> if ( r = { (/) } , { (/) , 1o } , r ) = { (/) , 1o } )
39 prex 
 |-  { (/) , 1o } e. _V
40 38 1 39 fvmpt 
 |-  ( { (/) } e. ~P 3o -> ( K ` { (/) } ) = { (/) , 1o } )
41 40 adantr 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> ( K ` { (/) } ) = { (/) , 1o } )
42 37 41 eleqtrrid 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> 1o e. ( K ` { (/) } ) )
43 1n0 
 |-  1o =/= (/)
44 43 neii 
 |-  -. 1o = (/)
45 eqcom 
 |-  ( 1o = 2o <-> 2o = 1o )
46 df-2o 
 |-  2o = suc 1o
47 df-1o 
 |-  1o = suc (/)
48 46 47 eqeq12i 
 |-  ( 2o = 1o <-> suc 1o = suc (/) )
49 suc11reg 
 |-  ( suc 1o = suc (/) <-> 1o = (/) )
50 45 48 49 3bitri 
 |-  ( 1o = 2o <-> 1o = (/) )
51 43 50 nemtbir 
 |-  -. 1o = 2o
52 44 51 pm3.2ni 
 |-  -. ( 1o = (/) \/ 1o = 2o )
53 elpri 
 |-  ( 1o e. { (/) , 2o } -> ( 1o = (/) \/ 1o = 2o ) )
54 52 53 mto 
 |-  -. 1o e. { (/) , 2o }
55 54 a1i 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> -. 1o e. { (/) , 2o } )
56 eqeq1 
 |-  ( r = { (/) , 2o } -> ( r = { (/) } <-> { (/) , 2o } = { (/) } ) )
57 id 
 |-  ( r = { (/) , 2o } -> r = { (/) , 2o } )
58 56 57 ifbieq2d 
 |-  ( r = { (/) , 2o } -> if ( r = { (/) } , { (/) , 1o } , r ) = if ( { (/) , 2o } = { (/) } , { (/) , 1o } , { (/) , 2o } ) )
59 15 prid2 
 |-  2o e. { (/) , 2o }
60 2on0 
 |-  2o =/= (/)
61 nelsn 
 |-  ( 2o =/= (/) -> -. 2o e. { (/) } )
62 60 61 ax-mp 
 |-  -. 2o e. { (/) }
63 nelneq2 
 |-  ( ( 2o e. { (/) , 2o } /\ -. 2o e. { (/) } ) -> -. { (/) , 2o } = { (/) } )
64 59 62 63 mp2an 
 |-  -. { (/) , 2o } = { (/) }
65 64 iffalsei 
 |-  if ( { (/) , 2o } = { (/) } , { (/) , 1o } , { (/) , 2o } ) = { (/) , 2o }
66 58 65 eqtrdi 
 |-  ( r = { (/) , 2o } -> if ( r = { (/) } , { (/) , 1o } , r ) = { (/) , 2o } )
67 prex 
 |-  { (/) , 2o } e. _V
68 66 1 67 fvmpt 
 |-  ( { (/) , 2o } e. ~P 3o -> ( K ` { (/) , 2o } ) = { (/) , 2o } )
69 68 adantl 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> ( K ` { (/) , 2o } ) = { (/) , 2o } )
70 55 69 neleqtrrd 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> -. 1o e. ( K ` { (/) , 2o } ) )
71 nelss 
 |-  ( ( 1o e. ( K ` { (/) } ) /\ -. 1o e. ( K ` { (/) , 2o } ) ) -> -. ( K ` { (/) } ) C_ ( K ` { (/) , 2o } ) )
72 42 70 71 syl2anc 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> -. ( K ` { (/) } ) C_ ( K ` { (/) , 2o } ) )
73 snsspr1 
 |-  { (/) } C_ { (/) , 2o }
74 72 73 jctil 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> ( { (/) } C_ { (/) , 2o } /\ -. ( K ` { (/) } ) C_ ( K ` { (/) , 2o } ) ) )
75 30 35 74 rspcedvd 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> E. t e. ~P 3o ( { (/) } C_ t /\ -. ( K ` { (/) } ) C_ ( K ` t ) ) )
76 22 29 75 rspcedvd 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> E. s e. ~P 3o E. t e. ~P 3o ( s C_ t /\ -. ( K ` s ) C_ ( K ` t ) ) )
77 7 21 76 mp2an 
 |-  E. s e. ~P 3o E. t e. ~P 3o ( s C_ t /\ -. ( K ` s ) C_ ( K ` t ) )