Theorem onsetreclem1

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

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

Proof

Step	Hyp	Ref	Expression
1		onsetreclem1.1	⊢ 𝐹 = ( 𝑥 ∈ V ↦ { ∪ 𝑥 , suc ∪ 𝑥 } )
2		unieq	⊢ ( 𝑥 = 𝑎 → ∪ 𝑥 = ∪ 𝑎 )
3		suceq	⊢ ( ∪ 𝑥 = ∪ 𝑎 → suc ∪ 𝑥 = suc ∪ 𝑎 )
4	2 3	syl	⊢ ( 𝑥 = 𝑎 → suc ∪ 𝑥 = suc ∪ 𝑎 )
5	2 4	preq12d	⊢ ( 𝑥 = 𝑎 → { ∪ 𝑥 , suc ∪ 𝑥 } = { ∪ 𝑎 , suc ∪ 𝑎 } )
6		prex	⊢ { ∪ 𝑎 , suc ∪ 𝑎 } ∈ V
7	5 1 6	fvmpt	⊢ ( 𝑎 ∈ V → ( 𝐹 ‘ 𝑎 ) = { ∪ 𝑎 , suc ∪ 𝑎 } )
8	7	elv	⊢ ( 𝐹 ‘ 𝑎 ) = { ∪ 𝑎 , suc ∪ 𝑎 }