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

Proof

Step	Hyp	Ref	Expression
1		clsk1indlem.k	⊢ 𝐾 = ( 𝑟 ∈ 𝒫 3o ↦ if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) )
2		id	⊢ ( 𝑠 = { ∅ } → 𝑠 = { ∅ } )
3		snsspr1	⊢ { ∅ } ⊆ { ∅ , 1o }
4	2 3	eqsstrdi	⊢ ( 𝑠 = { ∅ } → 𝑠 ⊆ { ∅ , 1o } )
5	4	ancli	⊢ ( 𝑠 = { ∅ } → ( 𝑠 = { ∅ } ∧ 𝑠 ⊆ { ∅ , 1o } ) )
6	5	con3i	⊢ ( ¬ ( 𝑠 = { ∅ } ∧ 𝑠 ⊆ { ∅ , 1o } ) → ¬ 𝑠 = { ∅ } )
7		ssid	⊢ 𝑠 ⊆ 𝑠
8	6 7	jctir	⊢ ( ¬ ( 𝑠 = { ∅ } ∧ 𝑠 ⊆ { ∅ , 1o } ) → ( ¬ 𝑠 = { ∅ } ∧ 𝑠 ⊆ 𝑠 ) )
9	8	orri	⊢ ( ( 𝑠 = { ∅ } ∧ 𝑠 ⊆ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑠 ⊆ 𝑠 ) )
10	9	a1i	⊢ ( 𝑠 ∈ 𝒫 3o → ( ( 𝑠 = { ∅ } ∧ 𝑠 ⊆ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑠 ⊆ 𝑠 ) ) )
11		sseq2	⊢ ( if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) = { ∅ , 1o } → ( 𝑠 ⊆ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ↔ 𝑠 ⊆ { ∅ , 1o } ) )
12		sseq2	⊢ ( if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) = 𝑠 → ( 𝑠 ⊆ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ↔ 𝑠 ⊆ 𝑠 ) )
13	11 12	elimif	⊢ ( 𝑠 ⊆ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ↔ ( ( 𝑠 = { ∅ } ∧ 𝑠 ⊆ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑠 ⊆ 𝑠 ) ) )
14	10 13	sylibr	⊢ ( 𝑠 ∈ 𝒫 3o → 𝑠 ⊆ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
15		eqeq1	⊢ ( 𝑟 = 𝑠 → ( 𝑟 = { ∅ } ↔ 𝑠 = { ∅ } ) )
16		id	⊢ ( 𝑟 = 𝑠 → 𝑟 = 𝑠 )
17	15 16	ifbieq2d	⊢ ( 𝑟 = 𝑠 → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
18		prex	⊢ { ∅ , 1o } ∈ V
19		vex	⊢ 𝑠 ∈ V
20	18 19	ifex	⊢ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∈ V
21	17 1 20	fvmpt	⊢ ( 𝑠 ∈ 𝒫 3o → ( 𝐾 ‘ 𝑠 ) = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
22	14 21	sseqtrrd	⊢ ( 𝑠 ∈ 𝒫 3o → 𝑠 ⊆ ( 𝐾 ‘ 𝑠 ) )
23	22	rgen	⊢ ∀ 𝑠 ∈ 𝒫 3o 𝑠 ⊆ ( 𝐾 ‘ 𝑠 )