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	⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) = ∅ )
Assertion	0setrec	⊢ ( 𝜑 → setrecs ( 𝐹 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		0setrec.1	⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) = ∅ )
2		eqid	⊢ setrecs ( 𝐹 ) = setrecs ( 𝐹 )
3		ss0	⊢ ( 𝑥 ⊆ ∅ → 𝑥 = ∅ )
4		fveq2	⊢ ( 𝑥 = ∅ → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ∅ ) )
5	4 1	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑥 = ∅ ) → ( 𝐹 ‘ 𝑥 ) = ∅ )
6	5	ex	⊢ ( 𝜑 → ( 𝑥 = ∅ → ( 𝐹 ‘ 𝑥 ) = ∅ ) )
7		eqimss	⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( 𝐹 ‘ 𝑥 ) ⊆ ∅ )
8	3 6 7	syl56	⊢ ( 𝜑 → ( 𝑥 ⊆ ∅ → ( 𝐹 ‘ 𝑥 ) ⊆ ∅ ) )
9	8	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ⊆ ∅ → ( 𝐹 ‘ 𝑥 ) ⊆ ∅ ) )
10	2 9	setrec2v	⊢ ( 𝜑 → setrecs ( 𝐹 ) ⊆ ∅ )
11		ss0	⊢ ( setrecs ( 𝐹 ) ⊆ ∅ → setrecs ( 𝐹 ) = ∅ )
12	10 11	syl	⊢ ( 𝜑 → setrecs ( 𝐹 ) = ∅ )