Metamath Proof Explorer


Theorem clsk1indlem2

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 K=r𝒫3𝑜ifr=1𝑜r
Assertion clsk1indlem2 s𝒫3𝑜sKs

Proof

Step Hyp Ref Expression
1 clsk1indlem.k K=r𝒫3𝑜ifr=1𝑜r
2 id s=s=
3 snsspr1 1𝑜
4 2 3 eqsstrdi s=s1𝑜
5 4 ancli s=s=s1𝑜
6 5 con3i ¬s=s1𝑜¬s=
7 ssid ss
8 6 7 jctir ¬s=s1𝑜¬s=ss
9 8 orri s=s1𝑜¬s=ss
10 9 a1i s𝒫3𝑜s=s1𝑜¬s=ss
11 sseq2 ifs=1𝑜s=1𝑜sifs=1𝑜ss1𝑜
12 sseq2 ifs=1𝑜s=ssifs=1𝑜sss
13 11 12 elimif sifs=1𝑜ss=s1𝑜¬s=ss
14 10 13 sylibr s𝒫3𝑜sifs=1𝑜s
15 eqeq1 r=sr=s=
16 id r=sr=s
17 15 16 ifbieq2d r=sifr=1𝑜r=ifs=1𝑜s
18 prex 1𝑜V
19 vex sV
20 18 19 ifex ifs=1𝑜sV
21 17 1 20 fvmpt s𝒫3𝑜Ks=ifs=1𝑜s
22 14 21 sseqtrrd s𝒫3𝑜sKs
23 22 rgen s𝒫3𝑜sKs