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 ⊢ A ∈ V
Assertion rdg0 ⊢ rec ⁡ F A ⁡ ∅ = A

Proof

Step Hyp Ref Expression
1 rdg.1 ⊢ A ∈ V
2 rdgdmlim ⊢ Lim ⁡ dom ⁡ rec ⁡ F A
3 limomss ⊢ Lim ⁡ dom ⁡ rec ⁡ F A → ω ⊆ dom ⁡ rec ⁡ F A
4 2 3 ax-mp ⊢ ω ⊆ dom ⁡ rec ⁡ F A
5 peano1 ⊢ ∅ ∈ ω
6 4 5 sselii ⊢ ∅ ∈ dom ⁡ rec ⁡ F A
7 eqid ⊢ x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x = x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x
8 rdgvalg ⊢ y ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ⁡ y = x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x ⁡ rec ⁡ F A ↾ y
9 7 8 1 tz7.44-1 ⊢ ∅ ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ⁡ ∅ = A
10 6 9 ax-mp ⊢ rec ⁡ F A ⁡ ∅ = A