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=\left(r\in 𝒫3_{𝑜}⟼if\left(r=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},r\right)\right)$$
Assertion	clsk1indlem4	$$⊢\forall s\in 𝒫3_{𝑜}K\left(K\left(s\right)\right)=K\left(s\right)$$

Proof

Step	Hyp	Ref	Expression
1		clsk1indlem.k	$$⊢K=\left(r\in 𝒫3_{𝑜}⟼if\left(r=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},r\right)\right)$$
2		tpex	$$⊢\left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}\in \mathrm{V}$$
3	2	a1i	$$⊢\top \to \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}\in \mathrm{V}$$
4		snsstp1	$$⊢\left\{\varnothing \right\}\subseteq \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
5	4	a1i	$$⊢\top \to \left\{\varnothing \right\}\subseteq \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
6		0ex	$$⊢\varnothing \in \mathrm{V}$$
7	6	snss	$$⊢\varnothing \in \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}\leftrightarrow \left\{\varnothing \right\}\subseteq \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
8	5 7	sylibr	$$⊢\top \to \varnothing \in \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
9		snsstp2	$$⊢\left\{1_{𝑜}\right\}\subseteq \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
10	9	a1i	$$⊢\top \to \left\{1_{𝑜}\right\}\subseteq \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
11		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
12	11	snss	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}\leftrightarrow \left\{1_{𝑜}\right\}\subseteq \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
13	10 12	sylibr	$$⊢\top \to 1_{𝑜}\in \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
14	8 13	prssd	$$⊢\top \to \left\{\varnothing ,1_{𝑜}\right\}\subseteq \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
15	3 14	sselpwd	$$⊢\top \to \left\{\varnothing ,1_{𝑜}\right\}\in 𝒫\left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
16	15	mptru	$$⊢\left\{\varnothing ,1_{𝑜}\right\}\in 𝒫\left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
17		df3o2	$$⊢3_{𝑜}=\left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
18	17	pweqi	$$⊢𝒫3_{𝑜}=𝒫\left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
19	16 18	eleqtrri	$$⊢\left\{\varnothing ,1_{𝑜}\right\}\in 𝒫3_{𝑜}$$
20	19	a1i	$$⊢s\in 𝒫3_{𝑜}\to \left\{\varnothing ,1_{𝑜}\right\}\in 𝒫3_{𝑜}$$
21		id	$$⊢s\in 𝒫3_{𝑜}\to s\in 𝒫3_{𝑜}$$
22	20 21	ifcld	$$⊢s\in 𝒫3_{𝑜}\to if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\in 𝒫3_{𝑜}$$
23		eqeq1	$$⊢r=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\to \left(r=\left\{\varnothing \right\}\leftrightarrow if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)=\left\{\varnothing \right\}\right)$$
24		eqcom	$$⊢if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)=\left\{\varnothing \right\}\leftrightarrow \left\{\varnothing \right\}=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)$$
25		eqif	$$⊢\left\{\varnothing \right\}=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\leftrightarrow \left(\left(s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}\right)\vee \left(\neg s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=s\right)\right)$$
26	24 25	bitri	$$⊢if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)=\left\{\varnothing \right\}\leftrightarrow \left(\left(s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}\right)\vee \left(\neg s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=s\right)\right)$$
27	23 26	bitrdi	$$⊢r=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\to \left(r=\left\{\varnothing \right\}\leftrightarrow \left(\left(s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}\right)\vee \left(\neg s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=s\right)\right)\right)$$
28		id	$$⊢r=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\to r=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)$$
29	27 28	ifbieq2d	$$⊢r=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\to if\left(r=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},r\right)=if\left(\left(\left(s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}\right)\vee \left(\neg s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=s\right)\right),\left\{\varnothing ,1_{𝑜}\right\},if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\right)$$
30		1n0	$$⊢1_{𝑜}\ne \varnothing$$
31		dfsn2	$$⊢\left\{\varnothing \right\}=\left\{\varnothing ,\varnothing \right\}$$
32	31	eqeq1i	$$⊢\left\{\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \left\{\varnothing ,\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}$$
33	6	a1i	$$⊢\top \to \varnothing \in \mathrm{V}$$
34		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
35	34	a1i	$$⊢\top \to 1_{𝑜}\in \mathrm{On}$$
36	33 35	preq2b	$$⊢\top \to \left(\left\{\varnothing ,\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \varnothing =1_{𝑜}\right)$$
37	36	mptru	$$⊢\left\{\varnothing ,\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \varnothing =1_{𝑜}$$
38		eqcom	$$⊢\varnothing =1_{𝑜}\leftrightarrow 1_{𝑜}=\varnothing$$
39	32 37 38	3bitri	$$⊢\left\{\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow 1_{𝑜}=\varnothing$$
40	30 39	nemtbir	$$⊢\neg \left\{\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}$$
41	40	intnan	$$⊢\neg \left(s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}\right)$$
42		pm3.24	$$⊢\neg \left(s=\left\{\varnothing \right\}\wedge \neg s=\left\{\varnothing \right\}\right)$$
43		eqcom	$$⊢s=\left\{\varnothing \right\}\leftrightarrow \left\{\varnothing \right\}=s$$
44	43	anbi2ci	$$⊢\left(s=\left\{\varnothing \right\}\wedge \neg s=\left\{\varnothing \right\}\right)\leftrightarrow \left(\neg s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=s\right)$$
45	42 44	mtbi	$$⊢\neg \left(\neg s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=s\right)$$
46	41 45	pm3.2ni	$$⊢\neg \left(\left(s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}\right)\vee \left(\neg s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=s\right)\right)$$
47	46	iffalsei	$$⊢if\left(\left(\left(s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=\left\{\varnothing ,1_{𝑜}\right\}\right)\vee \left(\neg s=\left\{\varnothing \right\}\wedge \left\{\varnothing \right\}=s\right)\right),\left\{\varnothing ,1_{𝑜}\right\},if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\right)=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)$$
48	29 47	eqtrdi	$$⊢r=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\to if\left(r=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},r\right)=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)$$
49		prex	$$⊢\left\{\varnothing ,1_{𝑜}\right\}\in \mathrm{V}$$
50		vex	$$⊢s\in \mathrm{V}$$
51	49 50	ifex	$$⊢if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\in \mathrm{V}$$
52	48 1 51	fvmpt	$$⊢if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\in 𝒫3_{𝑜}\to K\left(if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\right)=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)$$
53	22 52	syl	$$⊢s\in 𝒫3_{𝑜}\to K\left(if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\right)=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)$$
54		eqeq1	$$⊢r=s\to \left(r=\left\{\varnothing \right\}\leftrightarrow s=\left\{\varnothing \right\}\right)$$
55		id	$$⊢r=s\to r=s$$
56	54 55	ifbieq2d	$$⊢r=s\to if\left(r=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},r\right)=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)$$
57	56 1 51	fvmpt	$$⊢s\in 𝒫3_{𝑜}\to K\left(s\right)=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)$$
58	57	fveq2d	$$⊢s\in 𝒫3_{𝑜}\to K\left(K\left(s\right)\right)=K\left(if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\right)$$
59	53 58 57	3eqtr4d	$$⊢s\in 𝒫3_{𝑜}\to K\left(K\left(s\right)\right)=K\left(s\right)$$
60	59	rgen	$$⊢\forall s\in 𝒫3_{𝑜}K\left(K\left(s\right)\right)=K\left(s\right)$$