Metamath Proof Explorer

Theorem clsk1indlem4

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

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

Proof

Step Hyp Ref Expression
1 clsk1indlem.k 
 |-  K = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) )
2 tpex 
 |-  { (/) , 1o , 2o } e. _V
3 2 a1i 
 |-  ( T. -> { (/) , 1o , 2o } e. _V )
4 snsstp1 
 |-  { (/) } C_ { (/) , 1o , 2o }
5 4 a1i 
 |-  ( T. -> { (/) } C_ { (/) , 1o , 2o } )
6 0ex 
 |-  (/) e. _V
7 6 snss 
 |-  ( (/) e. { (/) , 1o , 2o } <-> { (/) } C_ { (/) , 1o , 2o } )
8 5 7 sylibr 
 |-  ( T. -> (/) e. { (/) , 1o , 2o } )
9 snsstp2 
 |-  { 1o } C_ { (/) , 1o , 2o }
10 9 a1i 
 |-  ( T. -> { 1o } C_ { (/) , 1o , 2o } )
11 1oex 
 |-  1o e. _V
12 11 snss 
 |-  ( 1o e. { (/) , 1o , 2o } <-> { 1o } C_ { (/) , 1o , 2o } )
13 10 12 sylibr 
 |-  ( T. -> 1o e. { (/) , 1o , 2o } )
14 8 13 prssd 
 |-  ( T. -> { (/) , 1o } C_ { (/) , 1o , 2o } )
15 3 14 sselpwd 
 |-  ( T. -> { (/) , 1o } e. ~P { (/) , 1o , 2o } )
16 15 mptru 
 |-  { (/) , 1o } e. ~P { (/) , 1o , 2o }
17 df3o2 
 |-  3o = { (/) , 1o , 2o }
18 17 pweqi 
 |-  ~P 3o = ~P { (/) , 1o , 2o }
19 16 18 eleqtrri 
 |-  { (/) , 1o } e. ~P 3o
20 19 a1i 
 |-  ( s e. ~P 3o -> { (/) , 1o } e. ~P 3o )
21 id 
 |-  ( s e. ~P 3o -> s e. ~P 3o )
22 20 21 ifcld 
 |-  ( s e. ~P 3o -> if ( s = { (/) } , { (/) , 1o } , s ) e. ~P 3o )
23 eqeq1 
 |-  ( r = if ( s = { (/) } , { (/) , 1o } , s ) -> ( r = { (/) } <-> if ( s = { (/) } , { (/) , 1o } , s ) = { (/) } ) )
24 eqcom 
 |-  ( if ( s = { (/) } , { (/) , 1o } , s ) = { (/) } <-> { (/) } = if ( s = { (/) } , { (/) , 1o } , s ) )
25 eqif 
 |-  ( { (/) } = if ( s = { (/) } , { (/) , 1o } , s ) <-> ( ( s = { (/) } /\ { (/) } = { (/) , 1o } ) \/ ( -. s = { (/) } /\ { (/) } = s ) ) )
26 24 25 bitri 
 |-  ( if ( s = { (/) } , { (/) , 1o } , s ) = { (/) } <-> ( ( s = { (/) } /\ { (/) } = { (/) , 1o } ) \/ ( -. s = { (/) } /\ { (/) } = s ) ) )
27 23 26 bitrdi 
 |-  ( r = if ( s = { (/) } , { (/) , 1o } , s ) -> ( r = { (/) } <-> ( ( s = { (/) } /\ { (/) } = { (/) , 1o } ) \/ ( -. s = { (/) } /\ { (/) } = s ) ) ) )
28 id 
 |-  ( r = if ( s = { (/) } , { (/) , 1o } , s ) -> r = if ( s = { (/) } , { (/) , 1o } , s ) )
29 27 28 ifbieq2d 
 |-  ( r = if ( s = { (/) } , { (/) , 1o } , s ) -> if ( r = { (/) } , { (/) , 1o } , r ) = if ( ( ( s = { (/) } /\ { (/) } = { (/) , 1o } ) \/ ( -. s = { (/) } /\ { (/) } = s ) ) , { (/) , 1o } , if ( s = { (/) } , { (/) , 1o } , s ) ) )
30 1n0 
 |-  1o =/= (/)
31 dfsn2 
 |-  { (/) } = { (/) , (/) }
32 31 eqeq1i 
 |-  ( { (/) } = { (/) , 1o } <-> { (/) , (/) } = { (/) , 1o } )
33 6 a1i 
 |-  ( T. -> (/) e. _V )
34 1on 
 |-  1o e. On
35 34 a1i 
 |-  ( T. -> 1o e. On )
36 33 35 preq2b 
 |-  ( T. -> ( { (/) , (/) } = { (/) , 1o } <-> (/) = 1o ) )
37 36 mptru 
 |-  ( { (/) , (/) } = { (/) , 1o } <-> (/) = 1o )
38 eqcom 
 |-  ( (/) = 1o <-> 1o = (/) )
39 32 37 38 3bitri 
 |-  ( { (/) } = { (/) , 1o } <-> 1o = (/) )
40 30 39 nemtbir 
 |-  -. { (/) } = { (/) , 1o }
41 40 intnan 
 |-  -. ( s = { (/) } /\ { (/) } = { (/) , 1o } )
42 pm3.24 
 |-  -. ( s = { (/) } /\ -. s = { (/) } )
43 eqcom 
 |-  ( s = { (/) } <-> { (/) } = s )
44 43 anbi2ci 
 |-  ( ( s = { (/) } /\ -. s = { (/) } ) <-> ( -. s = { (/) } /\ { (/) } = s ) )
45 42 44 mtbi 
 |-  -. ( -. s = { (/) } /\ { (/) } = s )
46 41 45 pm3.2ni 
 |-  -. ( ( s = { (/) } /\ { (/) } = { (/) , 1o } ) \/ ( -. s = { (/) } /\ { (/) } = s ) )
47 46 iffalsei 
 |-  if ( ( ( s = { (/) } /\ { (/) } = { (/) , 1o } ) \/ ( -. s = { (/) } /\ { (/) } = s ) ) , { (/) , 1o } , if ( s = { (/) } , { (/) , 1o } , s ) ) = if ( s = { (/) } , { (/) , 1o } , s )
48 29 47 eqtrdi 
 |-  ( r = if ( s = { (/) } , { (/) , 1o } , s ) -> if ( r = { (/) } , { (/) , 1o } , r ) = if ( s = { (/) } , { (/) , 1o } , s ) )
49 prex 
 |-  { (/) , 1o } e. _V
50 vex 
 |-  s e. _V
51 49 50 ifex 
 |-  if ( s = { (/) } , { (/) , 1o } , s ) e. _V
52 48 1 51 fvmpt 
 |-  ( if ( s = { (/) } , { (/) , 1o } , s ) e. ~P 3o -> ( K ` if ( s = { (/) } , { (/) , 1o } , s ) ) = if ( s = { (/) } , { (/) , 1o } , s ) )
53 22 52 syl 
 |-  ( s e. ~P 3o -> ( K ` if ( s = { (/) } , { (/) , 1o } , s ) ) = if ( s = { (/) } , { (/) , 1o } , s ) )
54 eqeq1 
 |-  ( r = s -> ( r = { (/) } <-> s = { (/) } ) )
55 id 
 |-  ( r = s -> r = s )
56 54 55 ifbieq2d 
 |-  ( r = s -> if ( r = { (/) } , { (/) , 1o } , r ) = if ( s = { (/) } , { (/) , 1o } , s ) )
57 56 1 51 fvmpt 
 |-  ( s e. ~P 3o -> ( K ` s ) = if ( s = { (/) } , { (/) , 1o } , s ) )
58 57 fveq2d 
 |-  ( s e. ~P 3o -> ( K ` ( K ` s ) ) = ( K ` if ( s = { (/) } , { (/) , 1o } , s ) ) )
59 53 58 57 3eqtr4d 
 |-  ( s e. ~P 3o -> ( K ` ( K ` s ) ) = ( K ` s ) )
60 59 rgen 
 |-  A. s e. ~P 3o ( K ` ( K ` s ) ) = ( K ` s )