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

Proof

Step	Hyp	Ref	Expression
1		clsk1indlem.k	|- K = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) )
2		id	|- ( s = { (/) } -> s = { (/) } )
3		snsspr1	|- { (/) } C_ { (/) , 1o }
4	2 3	eqsstrdi	|- ( s = { (/) } -> s C_ { (/) , 1o } )
5	4	ancli	|- ( s = { (/) } -> ( s = { (/) } /\ s C_ { (/) , 1o } ) )
6	5	con3i	|- ( -. ( s = { (/) } /\ s C_ { (/) , 1o } ) -> -. s = { (/) } )
7		ssid	|- s C_ s
8	6 7	jctir	|- ( -. ( s = { (/) } /\ s C_ { (/) , 1o } ) -> ( -. s = { (/) } /\ s C_ s ) )
9	8	orri	|- ( ( s = { (/) } /\ s C_ { (/) , 1o } ) \/ ( -. s = { (/) } /\ s C_ s ) )
10	9	a1i	|- ( s e. ~P 3o -> ( ( s = { (/) } /\ s C_ { (/) , 1o } ) \/ ( -. s = { (/) } /\ s C_ s ) ) )
11		sseq2	|- ( if ( s = { (/) } , { (/) , 1o } , s ) = { (/) , 1o } -> ( s C_ if ( s = { (/) } , { (/) , 1o } , s ) <-> s C_ { (/) , 1o } ) )
12		sseq2	|- ( if ( s = { (/) } , { (/) , 1o } , s ) = s -> ( s C_ if ( s = { (/) } , { (/) , 1o } , s ) <-> s C_ s ) )
13	11 12	elimif	|- ( s C_ if ( s = { (/) } , { (/) , 1o } , s ) <-> ( ( s = { (/) } /\ s C_ { (/) , 1o } ) \/ ( -. s = { (/) } /\ s C_ s ) ) )
14	10 13	sylibr	|- ( s e. ~P 3o -> s C_ if ( s = { (/) } , { (/) , 1o } , s ) )
15		eqeq1	|- ( r = s -> ( r = { (/) } <-> s = { (/) } ) )
16		id	|- ( r = s -> r = s )
17	15 16	ifbieq2d	|- ( r = s -> if ( r = { (/) } , { (/) , 1o } , r ) = if ( s = { (/) } , { (/) , 1o } , s ) )
18		prex	|- { (/) , 1o } e. _V
19		vex	|- s e. _V
20	18 19	ifex	|- if ( s = { (/) } , { (/) , 1o } , s ) e. _V
21	17 1 20	fvmpt	|- ( s e. ~P 3o -> ( K ` s ) = if ( s = { (/) } , { (/) , 1o } , s ) )
22	14 21	sseqtrrd	|- ( s e. ~P 3o -> s C_ ( K ` s ) )
23	22	rgen	|- A. s e. ~P 3o s C_ ( K ` s )