This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐹 , 𝐴 ) ‘ ∅ ) = 𝐴