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=\left(r\in 𝒫3_{𝑜}⟼if\left(r=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},r\right)\right)$$
Assertion	clsk1indlem2	$$⊢\forall s\in 𝒫3_{𝑜}s\subseteq 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		id	$$⊢s=\left\{\varnothing \right\}\to s=\left\{\varnothing \right\}$$
3		snsspr1	$$⊢\left\{\varnothing \right\}\subseteq \left\{\varnothing ,1_{𝑜}\right\}$$
4	2 3	eqsstrdi	$$⊢s=\left\{\varnothing \right\}\to s\subseteq \left\{\varnothing ,1_{𝑜}\right\}$$
5	4	ancli	$$⊢s=\left\{\varnothing \right\}\to \left(s=\left\{\varnothing \right\}\wedge s\subseteq \left\{\varnothing ,1_{𝑜}\right\}\right)$$
6	5	con3i	$$⊢\neg \left(s=\left\{\varnothing \right\}\wedge s\subseteq \left\{\varnothing ,1_{𝑜}\right\}\right)\to \neg s=\left\{\varnothing \right\}$$
7		ssid	$$⊢s\subseteq s$$
8	6 7	jctir	$$⊢\neg \left(s=\left\{\varnothing \right\}\wedge s\subseteq \left\{\varnothing ,1_{𝑜}\right\}\right)\to \left(\neg s=\left\{\varnothing \right\}\wedge s\subseteq s\right)$$
9	8	orri	$$⊢\left(\left(s=\left\{\varnothing \right\}\wedge s\subseteq \left\{\varnothing ,1_{𝑜}\right\}\right)\vee \left(\neg s=\left\{\varnothing \right\}\wedge s\subseteq s\right)\right)$$
10	9	a1i	$$⊢s\in 𝒫3_{𝑜}\to \left(\left(s=\left\{\varnothing \right\}\wedge s\subseteq \left\{\varnothing ,1_{𝑜}\right\}\right)\vee \left(\neg s=\left\{\varnothing \right\}\wedge s\subseteq s\right)\right)$$
11		sseq2	$$⊢if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)=\left\{\varnothing ,1_{𝑜}\right\}\to \left(s\subseteq if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\leftrightarrow s\subseteq \left\{\varnothing ,1_{𝑜}\right\}\right)$$
12		sseq2	$$⊢if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)=s\to \left(s\subseteq if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\leftrightarrow s\subseteq s\right)$$
13	11 12	elimif	$$⊢s\subseteq if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\leftrightarrow \left(\left(s=\left\{\varnothing \right\}\wedge s\subseteq \left\{\varnothing ,1_{𝑜}\right\}\right)\vee \left(\neg s=\left\{\varnothing \right\}\wedge s\subseteq s\right)\right)$$
14	10 13	sylibr	$$⊢s\in 𝒫3_{𝑜}\to s\subseteq if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)$$
15		eqeq1	$$⊢r=s\to \left(r=\left\{\varnothing \right\}\leftrightarrow s=\left\{\varnothing \right\}\right)$$
16		id	$$⊢r=s\to r=s$$
17	15 16	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)$$
18		prex	$$⊢\left\{\varnothing ,1_{𝑜}\right\}\in \mathrm{V}$$
19		vex	$$⊢s\in \mathrm{V}$$
20	18 19	ifex	$$⊢if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)\in \mathrm{V}$$
21	17 1 20	fvmpt	$$⊢s\in 𝒫3_{𝑜}\to K\left(s\right)=if\left(s=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},s\right)$$
22	14 21	sseqtrrd	$$⊢s\in 𝒫3_{𝑜}\to s\subseteq K\left(s\right)$$
23	22	rgen	$$⊢\forall s\in 𝒫3_{𝑜}s\subseteq K\left(s\right)$$