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 = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) )
Assertion	clsk1indlem0	|- ( K ` (/) ) = (/)

Proof

Step	Hyp	Ref	Expression
1		clsk1indlem.k	|- K = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) )
2		0elpw	|- (/) e. ~P 3o
3		eqeq1	|- ( r = (/) -> ( r = { (/) } <-> (/) = { (/) } ) )
4		id	|- ( r = (/) -> r = (/) )
5	3 4	ifbieq2d	|- ( r = (/) -> if ( r = { (/) } , { (/) , 1o } , r ) = if ( (/) = { (/) } , { (/) , 1o } , (/) ) )
6		0nep0	|- (/) =/= { (/) }
7	6	a1i	|- ( r = (/) -> (/) =/= { (/) } )
8	7	neneqd	|- ( r = (/) -> -. (/) = { (/) } )
9	8	iffalsed	|- ( r = (/) -> if ( (/) = { (/) } , { (/) , 1o } , (/) ) = (/) )
10	5 9	eqtrd	|- ( r = (/) -> if ( r = { (/) } , { (/) , 1o } , r ) = (/) )
11		0ex	|- (/) e. _V
12	10 1 11	fvmpt	|- ( (/) e. ~P 3o -> ( K ` (/) ) = (/) )
13	2 12	ax-mp	|- ( K ` (/) ) = (/)