Theorem clsk1indlem0

Description: The ansatz closure function ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) has the K0 property of preserving the nullary union. (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	clsk1indlem0	$$⊢K\left(\varnothing \right)=\varnothing$$

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		0elpw	$$⊢\varnothing \in 𝒫3_{𝑜}$$
3		eqeq1	$$⊢r=\varnothing \to \left(r=\left\{\varnothing \right\}\leftrightarrow \varnothing =\left\{\varnothing \right\}\right)$$
4		id	$$⊢r=\varnothing \to r=\varnothing$$
5	3 4	ifbieq2d	$$⊢r=\varnothing \to if\left(r=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},r\right)=if\left(\varnothing =\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},\varnothing \right)$$
6		0nep0	$$⊢\varnothing \ne \left\{\varnothing \right\}$$
7	6	a1i	$$⊢r=\varnothing \to \varnothing \ne \left\{\varnothing \right\}$$
8	7	neneqd	$$⊢r=\varnothing \to \neg \varnothing =\left\{\varnothing \right\}$$
9	8	iffalsed	$$⊢r=\varnothing \to if\left(\varnothing =\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},\varnothing \right)=\varnothing$$
10	5 9	eqtrd	$$⊢r=\varnothing \to if\left(r=\left\{\varnothing \right\},\left\{\varnothing ,1_{𝑜}\right\},r\right)=\varnothing$$
11		0ex	$$⊢\varnothing \in \mathrm{V}$$
12	10 1 11	fvmpt	$$⊢\varnothing \in 𝒫3_{𝑜}\to K\left(\varnothing \right)=\varnothing$$
13	2 12	ax-mp	$$⊢K\left(\varnothing \right)=\varnothing$$