Theorem rdg0

Description: The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995) (Revised by Mario Carneiro, 14-Nov-2014)

	Ref	Expression
Hypothesis	rdg.1	⊢ 𝐴 ∈ V
Assertion	rdg0	⊢ ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		rdg.1	⊢ 𝐴 ∈ V
2		rdgdmlim	⊢ Lim dom rec ( 𝐹 , 𝐴 )
3		limomss	⊢ ( Lim dom rec ( 𝐹 , 𝐴 ) → ω ⊆ dom rec ( 𝐹 , 𝐴 ) )
4	2 3	ax-mp	⊢ ω ⊆ dom rec ( 𝐹 , 𝐴 )
5		peano1	⊢ ∅ ∈ ω
6	4 5	sselii	⊢ ∅ ∈ dom rec ( 𝐹 , 𝐴 )
7		eqid	⊢ ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) = ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) )
8		rdgvalg	⊢ ( 𝑦 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ 𝑦 ) ) )
9	7 8 1	tz7.44-1	⊢ ( ∅ ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = 𝐴 )
10	6 9	ax-mp	⊢ ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = 𝐴