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

Proof

Step	Hyp	Ref	Expression
1		clsk1indlem.k	⊢ 𝐾 = ( 𝑟 ∈ 𝒫 3o ↦ if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) )
2		0elpw	⊢ ∅ ∈ 𝒫 3o
3		eqeq1	⊢ ( 𝑟 = ∅ → ( 𝑟 = { ∅ } ↔ ∅ = { ∅ } ) )
4		id	⊢ ( 𝑟 = ∅ → 𝑟 = ∅ )
5	3 4	ifbieq2d	⊢ ( 𝑟 = ∅ → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = if ( ∅ = { ∅ } , { ∅ , 1o } , ∅ ) )
6		0nep0	⊢ ∅ ≠ { ∅ }
7	6	a1i	⊢ ( 𝑟 = ∅ → ∅ ≠ { ∅ } )
8	7	neneqd	⊢ ( 𝑟 = ∅ → ¬ ∅ = { ∅ } )
9	8	iffalsed	⊢ ( 𝑟 = ∅ → if ( ∅ = { ∅ } , { ∅ , 1o } , ∅ ) = ∅ )
10	5 9	eqtrd	⊢ ( 𝑟 = ∅ → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = ∅ )
11		0ex	⊢ ∅ ∈ V
12	10 1 11	fvmpt	⊢ ( ∅ ∈ 𝒫 3o → ( 𝐾 ‘ ∅ ) = ∅ )
13	2 12	ax-mp	⊢ ( 𝐾 ‘ ∅ ) = ∅