Theorem setrecsss

Description: The setrecs operator respects the subset relation between two functions F and G . (Contributed by Emmett Weisz, 13-Mar-2022)

	Ref	Expression
Hypotheses	setrecsss.1	|- ( ph -> Fun G )
	setrecsss.2	|- ( ph -> F C_ G )
Assertion	setrecsss	|- ( ph -> setrecs ( F ) C_ setrecs ( G ) )

Proof

Step	Hyp	Ref	Expression
1		setrecsss.1	|- ( ph -> Fun G )
2		setrecsss.2	|- ( ph -> F C_ G )
3		eqid	|- setrecs ( F ) = setrecs ( F )
4		imass1	|- ( F C_ G -> ( F " { x } ) C_ ( G " { x } ) )
5	2 4	syl	|- ( ph -> ( F " { x } ) C_ ( G " { x } ) )
6	5	unissd	|- ( ph -> U. ( F " { x } ) C_ U. ( G " { x } ) )
7		funss	|- ( F C_ G -> ( Fun G -> Fun F ) )
8	2 1 7	sylc	|- ( ph -> Fun F )
9		funfv	|- ( Fun F -> ( F ` x ) = U. ( F " { x } ) )
10	8 9	syl	|- ( ph -> ( F ` x ) = U. ( F " { x } ) )
11		funfv	|- ( Fun G -> ( G ` x ) = U. ( G " { x } ) )
12	1 11	syl	|- ( ph -> ( G ` x ) = U. ( G " { x } ) )
13	6 10 12	3sstr4d	|- ( ph -> ( F ` x ) C_ ( G ` x ) )
14	13	adantr	|- ( ( ph /\ x C_ setrecs ( G ) ) -> ( F ` x ) C_ ( G ` x ) )
15		eqid	|- setrecs ( G ) = setrecs ( G )
16		vex	|- x e. _V
17	16	a1i	|- ( ( ph /\ x C_ setrecs ( G ) ) -> x e. _V )
18		simpr	|- ( ( ph /\ x C_ setrecs ( G ) ) -> x C_ setrecs ( G ) )
19	15 17 18	setrec1	|- ( ( ph /\ x C_ setrecs ( G ) ) -> ( G ` x ) C_ setrecs ( G ) )
20	14 19	sstrd	|- ( ( ph /\ x C_ setrecs ( G ) ) -> ( F ` x ) C_ setrecs ( G ) )
21	20	ex	|- ( ph -> ( x C_ setrecs ( G ) -> ( F ` x ) C_ setrecs ( G ) ) )
22	21	alrimiv	|- ( ph -> A. x ( x C_ setrecs ( G ) -> ( F ` x ) C_ setrecs ( G ) ) )
23	3 22	setrec2v	|- ( ph -> setrecs ( F ) C_ setrecs ( G ) )