Theorem onsetreclem2

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

	Ref	Expression
Hypothesis	onsetreclem2.1	⊢ 𝐹 = ( 𝑥 ∈ V ↦ { ∪ 𝑥 , suc ∪ 𝑥 } )
Assertion	onsetreclem2	⊢ ( 𝑎 ⊆ On → ( 𝐹 ‘ 𝑎 ) ⊆ On )

Proof

Step	Hyp	Ref	Expression
1		onsetreclem2.1	⊢ 𝐹 = ( 𝑥 ∈ V ↦ { ∪ 𝑥 , suc ∪ 𝑥 } )
2	1	onsetreclem1	⊢ ( 𝐹 ‘ 𝑎 ) = { ∪ 𝑎 , suc ∪ 𝑎 }
3		vex	⊢ 𝑎 ∈ V
4	3	ssonunii	⊢ ( 𝑎 ⊆ On → ∪ 𝑎 ∈ On )
5		suceloni	⊢ ( ∪ 𝑎 ∈ On → suc ∪ 𝑎 ∈ On )
6		prssi	⊢ ( ( ∪ 𝑎 ∈ On ∧ suc ∪ 𝑎 ∈ On ) → { ∪ 𝑎 , suc ∪ 𝑎 } ⊆ On )
7	4 5 6	syl2anc2	⊢ ( 𝑎 ⊆ On → { ∪ 𝑎 , suc ∪ 𝑎 } ⊆ On )
8	2 7	eqsstrid	⊢ ( 𝑎 ⊆ On → ( 𝐹 ‘ 𝑎 ) ⊆ On )