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