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 𝑜 if r = 1 𝑜 r
Assertion clsk1indlem4 s 𝒫 3 𝑜 K K s = K s

Proof

Step Hyp Ref Expression
1 clsk1indlem.k K = r 𝒫 3 𝑜 if r = 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 𝑜 if s = 1 𝑜 s 𝒫 3 𝑜
23 eqeq1 r = if s = 1 𝑜 s r = if s = 1 𝑜 s =
24 eqcom if s = 1 𝑜 s = = if s = 1 𝑜 s
25 eqif = if s = 1 𝑜 s s = = 1 𝑜 ¬ s = = s
26 24 25 bitri if s = 1 𝑜 s = s = = 1 𝑜 ¬ s = = s
27 23 26 bitrdi r = if s = 1 𝑜 s r = s = = 1 𝑜 ¬ s = = s
28 id r = if s = 1 𝑜 s r = if s = 1 𝑜 s
29 27 28 ifbieq2d r = if s = 1 𝑜 s if r = 1 𝑜 r = if s = = 1 𝑜 ¬ s = = s 1 𝑜 if s = 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 if s = = 1 𝑜 ¬ s = = s 1 𝑜 if s = 1 𝑜 s = if s = 1 𝑜 s
48 29 47 eqtrdi r = if s = 1 𝑜 s if r = 1 𝑜 r = if s = 1 𝑜 s
49 prex 1 𝑜 V
50 vex s V
51 49 50 ifex if s = 1 𝑜 s V
52 48 1 51 fvmpt if s = 1 𝑜 s 𝒫 3 𝑜 K if s = 1 𝑜 s = if s = 1 𝑜 s
53 22 52 syl s 𝒫 3 𝑜 K if s = 1 𝑜 s = if s = 1 𝑜 s
54 eqeq1 r = s r = s =
55 id r = s r = s
56 54 55 ifbieq2d r = s if r = 1 𝑜 r = if s = 1 𝑜 s
57 56 1 51 fvmpt s 𝒫 3 𝑜 K s = if s = 1 𝑜 s
58 57 fveq2d s 𝒫 3 𝑜 K K s = K if s = 1 𝑜 s
59 53 58 57 3eqtr4d s 𝒫 3 𝑜 K K s = K s
60 59 rgen s 𝒫 3 𝑜 K K s = K s