Theorem 0setrec

Description: If a function sends the empty set to itself, the function will not recursively generate any sets, regardless of its other values. (Contributed by Emmett Weisz, 23-Jun-2021)

	Ref	Expression
Hypothesis	0setrec.1	|- ( ph -> ( F ` (/) ) = (/) )
Assertion	0setrec	|- ( ph -> setrecs ( F ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		0setrec.1	|- ( ph -> ( F ` (/) ) = (/) )
2		eqid	|- setrecs ( F ) = setrecs ( F )
3		ss0	|- ( x C_ (/) -> x = (/) )
4		fveq2	|- ( x = (/) -> ( F ` x ) = ( F ` (/) ) )
5	4 1	sylan9eqr	|- ( ( ph /\ x = (/) ) -> ( F ` x ) = (/) )
6	5	ex	|- ( ph -> ( x = (/) -> ( F ` x ) = (/) ) )
7		eqimss	|- ( ( F ` x ) = (/) -> ( F ` x ) C_ (/) )
8	3 6 7	syl56	|- ( ph -> ( x C_ (/) -> ( F ` x ) C_ (/) ) )
9	8	alrimiv	|- ( ph -> A. x ( x C_ (/) -> ( F ` x ) C_ (/) ) )
10	2 9	setrec2v	|- ( ph -> setrecs ( F ) C_ (/) )
11		ss0	|- ( setrecs ( F ) C_ (/) -> setrecs ( F ) = (/) )
12	10 11	syl	|- ( ph -> setrecs ( F ) = (/) )