Theorem onsetreclem3

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

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

Proof

Step	Hyp	Ref	Expression
1		onsetreclem3.1	|- F = ( x e. _V |-> { U. x , suc U. x } )
2		eloni	|- ( a e. On -> Ord a )
3		orduniorsuc	|- ( Ord a -> ( a = U. a \/ a = suc U. a ) )
4	2 3	syl	|- ( a e. On -> ( a = U. a \/ a = suc U. a ) )
5		vex	|- a e. _V
6	5	elpr	|- ( a e. { U. a , suc U. a } <-> ( a = U. a \/ a = suc U. a ) )
7	4 6	sylibr	|- ( a e. On -> a e. { U. a , suc U. a } )
8	1	onsetreclem1	|- ( F ` a ) = { U. a , suc U. a }
9	7 8	eleqtrrdi	|- ( a e. On -> a e. ( F ` a ) )