Theorem onsetreclem2

Description: Lemma for onsetrec . (Contributed by Emmett Weisz, 22-Jun-2021) (New usage is discouraged.)

	Ref	Expression
Hypothesis	onsetreclem2.1	|- F = ( x e. _V |-> { U. x , suc U. x } )
Assertion	onsetreclem2	|- ( a C_ On -> ( F ` a ) C_ On )

Proof

Step	Hyp	Ref	Expression
1		onsetreclem2.1	|- F = ( x e. _V |-> { U. x , suc U. x } )
2	1	onsetreclem1	|- ( F ` a ) = { U. a , suc U. a }
3		vex	|- a e. _V
4	3	ssonunii	|- ( a C_ On -> U. a e. On )
5		suceloni	|- ( U. a e. On -> suc U. a e. On )
6		prssi	|- ( ( U. a e. On /\ suc U. a e. On ) -> { U. a , suc U. a } C_ On )
7	4 5 6	syl2anc2	|- ( a C_ On -> { U. a , suc U. a } C_ On )
8	2 7	eqsstrid	|- ( a C_ On -> ( F ` a ) C_ On )