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𝒫3𝑜ifr=1𝑜r
Assertion clsk1indlem4 s𝒫3𝑜KKs=Ks

Proof

Step Hyp Ref Expression
1 clsk1indlem.k K=r𝒫3𝑜ifr=1𝑜r
2 tpex 1𝑜2𝑜V
3 2 a1i 1𝑜2𝑜V
4 snsstp1 1𝑜2𝑜
5 4 a1i 1𝑜2𝑜
6 0ex V
7 6 snss 1𝑜2𝑜1𝑜2𝑜
8 5 7 sylibr 1𝑜2𝑜
9 snsstp2 1𝑜1𝑜2𝑜
10 9 a1i 1𝑜1𝑜2𝑜
11 1oex 1𝑜V
12 11 snss 1𝑜1𝑜2𝑜1𝑜1𝑜2𝑜
13 10 12 sylibr 1𝑜1𝑜2𝑜
14 8 13 prssd 1𝑜1𝑜2𝑜
15 3 14 sselpwd 1𝑜𝒫1𝑜2𝑜
16 15 mptru 1𝑜𝒫1𝑜2𝑜
17 df3o2 3𝑜=1𝑜2𝑜
18 17 pweqi 𝒫3𝑜=𝒫1𝑜2𝑜
19 16 18 eleqtrri 1𝑜𝒫3𝑜
20 19 a1i s𝒫3𝑜1𝑜𝒫3𝑜
21 id s𝒫3𝑜s𝒫3𝑜
22 20 21 ifcld s𝒫3𝑜ifs=1𝑜s𝒫3𝑜
23 eqeq1 r=ifs=1𝑜sr=ifs=1𝑜s=
24 eqcom ifs=1𝑜s==ifs=1𝑜s
25 eqif =ifs=1𝑜ss==1𝑜¬s==s
26 24 25 bitri ifs=1𝑜s=s==1𝑜¬s==s
27 23 26 bitrdi r=ifs=1𝑜sr=s==1𝑜¬s==s
28 id r=ifs=1𝑜sr=ifs=1𝑜s
29 27 28 ifbieq2d r=ifs=1𝑜sifr=1𝑜r=ifs==1𝑜¬s==s1𝑜ifs=1𝑜s
30 1n0 1𝑜
31 dfsn2 =
32 31 eqeq1i =1𝑜=1𝑜
33 6 a1i V
34 1on 1𝑜On
35 34 a1i 1𝑜On
36 33 35 preq2b =1𝑜=1𝑜
37 36 mptru =1𝑜=1𝑜
38 eqcom =1𝑜1𝑜=
39 32 37 38 3bitri =1𝑜1𝑜=
40 30 39 nemtbir ¬=1𝑜
41 40 intnan ¬s==1𝑜
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==1𝑜¬s==s
47 46 iffalsei ifs==1𝑜¬s==s1𝑜ifs=1𝑜s=ifs=1𝑜s
48 29 47 eqtrdi r=ifs=1𝑜sifr=1𝑜r=ifs=1𝑜s
49 prex 1𝑜V
50 vex sV
51 49 50 ifex ifs=1𝑜sV
52 48 1 51 fvmpt ifs=1𝑜s𝒫3𝑜Kifs=1𝑜s=ifs=1𝑜s
53 22 52 syl s𝒫3𝑜Kifs=1𝑜s=ifs=1𝑜s
54 eqeq1 r=sr=s=
55 id r=sr=s
56 54 55 ifbieq2d r=sifr=1𝑜r=ifs=1𝑜s
57 56 1 51 fvmpt s𝒫3𝑜Ks=ifs=1𝑜s
58 57 fveq2d s𝒫3𝑜KKs=Kifs=1𝑜s
59 53 58 57 3eqtr4d s𝒫3𝑜KKs=Ks
60 59 rgen s𝒫3𝑜KKs=Ks