Theorem setrec2mpt

Description: Version of setrec2 where F is defined using maps-to notation. Deduction form is omitted in the second hypothesis for simplicity. In practice, nothing important is lost since we are only interested in one choice of A , S , and V at a time. However, we are interested in what happens when C varies, so deduction form is used in the third hypothesis. (Contributed by Emmett Weisz, 4-Jun-2024)

	Ref	Expression
Hypotheses	setrec2mpt.1	|- B = setrecs ( ( a e. A |-> S ) )
	setrec2mpt.2	|- ( a e. A -> S e. V )
	setrec2mpt.3	|- ( ph -> A. a ( a C_ C -> S C_ C ) )
Assertion	setrec2mpt	|- ( ph -> B C_ C )

Proof

Step	Hyp	Ref	Expression
1		setrec2mpt.1	|- B = setrecs ( ( a e. A |-> S ) )
2		setrec2mpt.2	|- ( a e. A -> S e. V )
3		setrec2mpt.3	|- ( ph -> A. a ( a C_ C -> S C_ C ) )
4		nfmpt1	|- F/_ a ( a e. A |-> S )
5		eqid	|- ( a e. A |-> S ) = ( a e. A |-> S )
6	5	fvmpt2	|- ( ( a e. A /\ S e. V ) -> ( ( a e. A |-> S ) ` a ) = S )
7		eqimss	|- ( ( ( a e. A |-> S ) ` a ) = S -> ( ( a e. A |-> S ) ` a ) C_ S )
8	6 7	syl	|- ( ( a e. A /\ S e. V ) -> ( ( a e. A |-> S ) ` a ) C_ S )
9	2 8	mpdan	|- ( a e. A -> ( ( a e. A |-> S ) ` a ) C_ S )
10	5	fvmptndm	|- ( -. a e. A -> ( ( a e. A |-> S ) ` a ) = (/) )
11		0ss	|- (/) C_ S
12	10 11	eqsstrdi	|- ( -. a e. A -> ( ( a e. A |-> S ) ` a ) C_ S )
13	9 12	pm2.61i	|- ( ( a e. A |-> S ) ` a ) C_ S
14		sstr2	|- ( ( ( a e. A |-> S ) ` a ) C_ S -> ( S C_ C -> ( ( a e. A |-> S ) ` a ) C_ C ) )
15	13 14	ax-mp	|- ( S C_ C -> ( ( a e. A |-> S ) ` a ) C_ C )
16	15	imim2i	|- ( ( a C_ C -> S C_ C ) -> ( a C_ C -> ( ( a e. A |-> S ) ` a ) C_ C ) )
17	3 16	sylg	|- ( ph -> A. a ( a C_ C -> ( ( a e. A |-> S ) ` a ) C_ C ) )
18	4 1 17	setrec2	|- ( ph -> B C_ C )