Theorem onsetreclem3

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

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

Proof

Step	Hyp	Ref	Expression
1		onsetreclem3.1	⊢ 𝐹 = ( 𝑥 ∈ V ↦ { ∪ 𝑥 , suc ∪ 𝑥 } )
2		eloni	⊢ ( 𝑎 ∈ On → Ord 𝑎 )
3		orduniorsuc	⊢ ( Ord 𝑎 → ( 𝑎 = ∪ 𝑎 ∨ 𝑎 = suc ∪ 𝑎 ) )
4	2 3	syl	⊢ ( 𝑎 ∈ On → ( 𝑎 = ∪ 𝑎 ∨ 𝑎 = suc ∪ 𝑎 ) )
5		vex	⊢ 𝑎 ∈ V
6	5	elpr	⊢ ( 𝑎 ∈ { ∪ 𝑎 , suc ∪ 𝑎 } ↔ ( 𝑎 = ∪ 𝑎 ∨ 𝑎 = suc ∪ 𝑎 ) )
7	4 6	sylibr	⊢ ( 𝑎 ∈ On → 𝑎 ∈ { ∪ 𝑎 , suc ∪ 𝑎 } )
8	1	onsetreclem1	⊢ ( 𝐹 ‘ 𝑎 ) = { ∪ 𝑎 , suc ∪ 𝑎 }
9	7 8	eleqtrrdi	⊢ ( 𝑎 ∈ On → 𝑎 ∈ ( 𝐹 ‘ 𝑎 ) )