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	⊢ 𝐾 = ( 𝑟 ∈ 𝒫 3o ↦ if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) )
Assertion	clsk1indlem4	⊢ ∀ 𝑠 ∈ 𝒫 3o ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐾 ‘ 𝑠 )

Proof

Step	Hyp	Ref	Expression
1		clsk1indlem.k	⊢ 𝐾 = ( 𝑟 ∈ 𝒫 3o ↦ if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) )
2		tpex	⊢ { ∅ , 1o , 2o } ∈ V
3	2	a1i	⊢ ( ⊤ → { ∅ , 1o , 2o } ∈ V )
4		snsstp1	⊢ { ∅ } ⊆ { ∅ , 1o , 2o }
5	4	a1i	⊢ ( ⊤ → { ∅ } ⊆ { ∅ , 1o , 2o } )
6		0ex	⊢ ∅ ∈ V
7	6	snss	⊢ ( ∅ ∈ { ∅ , 1o , 2o } ↔ { ∅ } ⊆ { ∅ , 1o , 2o } )
8	5 7	sylibr	⊢ ( ⊤ → ∅ ∈ { ∅ , 1o , 2o } )
9		snsstp2	⊢ { 1o } ⊆ { ∅ , 1o , 2o }
10	9	a1i	⊢ ( ⊤ → { 1o } ⊆ { ∅ , 1o , 2o } )
11		1oex	⊢ 1o ∈ V
12	11	snss	⊢ ( 1o ∈ { ∅ , 1o , 2o } ↔ { 1o } ⊆ { ∅ , 1o , 2o } )
13	10 12	sylibr	⊢ ( ⊤ → 1o ∈ { ∅ , 1o , 2o } )
14	8 13	prssd	⊢ ( ⊤ → { ∅ , 1o } ⊆ { ∅ , 1o , 2o } )
15	3 14	sselpwd	⊢ ( ⊤ → { ∅ , 1o } ∈ 𝒫 { ∅ , 1o , 2o } )
16	15	mptru	⊢ { ∅ , 1o } ∈ 𝒫 { ∅ , 1o , 2o }
17		df3o2	⊢ 3o = { ∅ , 1o , 2o }
18	17	pweqi	⊢ 𝒫 3o = 𝒫 { ∅ , 1o , 2o }
19	16 18	eleqtrri	⊢ { ∅ , 1o } ∈ 𝒫 3o
20	19	a1i	⊢ ( 𝑠 ∈ 𝒫 3o → { ∅ , 1o } ∈ 𝒫 3o )
21		id	⊢ ( 𝑠 ∈ 𝒫 3o → 𝑠 ∈ 𝒫 3o )
22	20 21	ifcld	⊢ ( 𝑠 ∈ 𝒫 3o → if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∈ 𝒫 3o )
23		eqeq1	⊢ ( 𝑟 = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) → ( 𝑟 = { ∅ } ↔ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) = { ∅ } ) )
24		eqcom	⊢ ( if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) = { ∅ } ↔ { ∅ } = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
25		eqif	⊢ ( { ∅ } = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ↔ ( ( 𝑠 = { ∅ } ∧ { ∅ } = { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ { ∅ } = 𝑠 ) ) )
26	24 25	bitri	⊢ ( if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) = { ∅ } ↔ ( ( 𝑠 = { ∅ } ∧ { ∅ } = { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ { ∅ } = 𝑠 ) ) )
27	23 26	bitrdi	⊢ ( 𝑟 = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) → ( 𝑟 = { ∅ } ↔ ( ( 𝑠 = { ∅ } ∧ { ∅ } = { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ { ∅ } = 𝑠 ) ) ) )
28		id	⊢ ( 𝑟 = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) → 𝑟 = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
29	27 28	ifbieq2d	⊢ ( 𝑟 = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = if ( ( ( 𝑠 = { ∅ } ∧ { ∅ } = { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ { ∅ } = 𝑠 ) ) , { ∅ , 1o } , if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ) )
30		1n0	⊢ 1o ≠ ∅
31		dfsn2	⊢ { ∅ } = { ∅ , ∅ }
32	31	eqeq1i	⊢ ( { ∅ } = { ∅ , 1o } ↔ { ∅ , ∅ } = { ∅ , 1o } )
33	6	a1i	⊢ ( ⊤ → ∅ ∈ V )
34		1on	⊢ 1o ∈ On
35	34	a1i	⊢ ( ⊤ → 1o ∈ On )
36	33 35	preq2b	⊢ ( ⊤ → ( { ∅ , ∅ } = { ∅ , 1o } ↔ ∅ = 1o ) )
37	36	mptru	⊢ ( { ∅ , ∅ } = { ∅ , 1o } ↔ ∅ = 1o )
38		eqcom	⊢ ( ∅ = 1o ↔ 1o = ∅ )
39	32 37 38	3bitri	⊢ ( { ∅ } = { ∅ , 1o } ↔ 1o = ∅ )
40	30 39	nemtbir	⊢ ¬ { ∅ } = { ∅ , 1o }
41	40	intnan	⊢ ¬ ( 𝑠 = { ∅ } ∧ { ∅ } = { ∅ , 1o } )
42		pm3.24	⊢ ¬ ( 𝑠 = { ∅ } ∧ ¬ 𝑠 = { ∅ } )
43		eqcom	⊢ ( 𝑠 = { ∅ } ↔ { ∅ } = 𝑠 )
44	43	anbi2ci	⊢ ( ( 𝑠 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) ↔ ( ¬ 𝑠 = { ∅ } ∧ { ∅ } = 𝑠 ) )
45	42 44	mtbi	⊢ ¬ ( ¬ 𝑠 = { ∅ } ∧ { ∅ } = 𝑠 )
46	41 45	pm3.2ni	⊢ ¬ ( ( 𝑠 = { ∅ } ∧ { ∅ } = { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ { ∅ } = 𝑠 ) )
47	46	iffalsei	⊢ if ( ( ( 𝑠 = { ∅ } ∧ { ∅ } = { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ { ∅ } = 𝑠 ) ) , { ∅ , 1o } , if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ) = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 )
48	29 47	eqtrdi	⊢ ( 𝑟 = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
49		prex	⊢ { ∅ , 1o } ∈ V
50		vex	⊢ 𝑠 ∈ V
51	49 50	ifex	⊢ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∈ V
52	48 1 51	fvmpt	⊢ ( if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∈ 𝒫 3o → ( 𝐾 ‘ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ) = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
53	22 52	syl	⊢ ( 𝑠 ∈ 𝒫 3o → ( 𝐾 ‘ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ) = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
54		eqeq1	⊢ ( 𝑟 = 𝑠 → ( 𝑟 = { ∅ } ↔ 𝑠 = { ∅ } ) )
55		id	⊢ ( 𝑟 = 𝑠 → 𝑟 = 𝑠 )
56	54 55	ifbieq2d	⊢ ( 𝑟 = 𝑠 → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
57	56 1 51	fvmpt	⊢ ( 𝑠 ∈ 𝒫 3o → ( 𝐾 ‘ 𝑠 ) = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
58	57	fveq2d	⊢ ( 𝑠 ∈ 𝒫 3o → ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐾 ‘ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ) )
59	53 58 57	3eqtr4d	⊢ ( 𝑠 ∈ 𝒫 3o → ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐾 ‘ 𝑠 ) )
60	59	rgen	⊢ ∀ 𝑠 ∈ 𝒫 3o ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐾 ‘ 𝑠 )