Description: The ansatz closure function ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) has the K2 property of expanding. (Contributed by RP, 6-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | clsk1indlem.k | |
|
Assertion | clsk1indlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clsk1indlem.k | |
|
2 | id | |
|
3 | snsspr1 | |
|
4 | 2 3 | eqsstrdi | |
5 | 4 | ancli | |
6 | 5 | con3i | |
7 | ssid | |
|
8 | 6 7 | jctir | |
9 | 8 | orri | |
10 | 9 | a1i | |
11 | sseq2 | |
|
12 | sseq2 | |
|
13 | 11 12 | elimif | |
14 | 10 13 | sylibr | |
15 | eqeq1 | |
|
16 | id | |
|
17 | 15 16 | ifbieq2d | |
18 | prex | |
|
19 | vex | |
|
20 | 18 19 | ifex | |
21 | 17 1 20 | fvmpt | |
22 | 14 21 | sseqtrrd | |
23 | 22 | rgen | |