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 1oelpr 
 |-  1o e. { (/) , 1o }
37 iftrue 
 |-  ( r = { (/) } -> if ( r = { (/) } , { (/) , 1o } , r ) = { (/) , 1o } )
38 prex 
 |-  { (/) , 1o } e. _V
39 37 1 38 fvmpt 
 |-  ( { (/) } e. ~P 3o -> ( K ` { (/) } ) = { (/) , 1o } )
40 39 adantr 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> ( K ` { (/) } ) = { (/) , 1o } )
41 36 40 eleqtrrid 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> 1o e. ( K ` { (/) } ) )
42 1n0 
 |-  1o =/= (/)
43 42 neii 
 |-  -. 1o = (/)
44 eqcom 
 |-  ( 1o = 2o <-> 2o = 1o )
45 df-2o 
 |-  2o = suc 1o
46 df-1o 
 |-  1o = suc (/)
47 45 46 eqeq12i 
 |-  ( 2o = 1o <-> suc 1o = suc (/) )
48 suc11reg 
 |-  ( suc 1o = suc (/) <-> 1o = (/) )
49 44 47 48 3bitri 
 |-  ( 1o = 2o <-> 1o = (/) )
50 42 49 nemtbir 
 |-  -. 1o = 2o
51 43 50 pm3.2ni 
 |-  -. ( 1o = (/) \/ 1o = 2o )
52 elpri 
 |-  ( 1o e. { (/) , 2o } -> ( 1o = (/) \/ 1o = 2o ) )
53 51 52 mto 
 |-  -. 1o e. { (/) , 2o }
54 53 a1i 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> -. 1o e. { (/) , 2o } )
55 eqeq1 
 |-  ( r = { (/) , 2o } -> ( r = { (/) } <-> { (/) , 2o } = { (/) } ) )
56 id 
 |-  ( r = { (/) , 2o } -> r = { (/) , 2o } )
57 55 56 ifbieq2d 
 |-  ( r = { (/) , 2o } -> if ( r = { (/) } , { (/) , 1o } , r ) = if ( { (/) , 2o } = { (/) } , { (/) , 1o } , { (/) , 2o } ) )
58 15 prid2 
 |-  2o e. { (/) , 2o }
59 2on0 
 |-  2o =/= (/)
60 nelsn 
 |-  ( 2o =/= (/) -> -. 2o e. { (/) } )
61 59 60 ax-mp 
 |-  -. 2o e. { (/) }
62 nelneq2 
 |-  ( ( 2o e. { (/) , 2o } /\ -. 2o e. { (/) } ) -> -. { (/) , 2o } = { (/) } )
63 58 61 62 mp2an 
 |-  -. { (/) , 2o } = { (/) }
64 63 iffalsei 
 |-  if ( { (/) , 2o } = { (/) } , { (/) , 1o } , { (/) , 2o } ) = { (/) , 2o }
65 57 64 eqtrdi 
 |-  ( r = { (/) , 2o } -> if ( r = { (/) } , { (/) , 1o } , r ) = { (/) , 2o } )
66 prex 
 |-  { (/) , 2o } e. _V
67 65 1 66 fvmpt 
 |-  ( { (/) , 2o } e. ~P 3o -> ( K ` { (/) , 2o } ) = { (/) , 2o } )
68 67 adantl 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> ( K ` { (/) , 2o } ) = { (/) , 2o } )
69 54 68 neleqtrrd 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> -. 1o e. ( K ` { (/) , 2o } ) )
70 nelss 
 |-  ( ( 1o e. ( K ` { (/) } ) /\ -. 1o e. ( K ` { (/) , 2o } ) ) -> -. ( K ` { (/) } ) C_ ( K ` { (/) , 2o } ) )
71 41 69 70 syl2anc 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> -. ( K ` { (/) } ) C_ ( K ` { (/) , 2o } ) )
72 snsspr1 
 |-  { (/) } C_ { (/) , 2o }
73 71 72 jctil 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> ( { (/) } C_ { (/) , 2o } /\ -. ( K ` { (/) } ) C_ ( K ` { (/) , 2o } ) ) )
74 30 35 73 rspcedvd 
 |-  ( ( { (/) } e. ~P 3o /\ { (/) , 2o } e. ~P 3o ) -> E. t e. ~P 3o ( { (/) } C_ t /\ -. ( K ` { (/) } ) C_ ( K ` t ) ) )
75 22 29 74 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 ) ) )
76 7 21 75 mp2an 
 |-  E. s e. ~P 3o E. t e. ~P 3o ( s C_ t /\ -. ( K ` s ) C_ ( K ` t ) )