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

Metamath Proof Explorer

Theorem rdg0n

Description: If A is a proper class, then the recursive function generator at (/) is the empty set. (Contributed by Scott Fenton, 31-Oct-2024)

Ref Expression
Assertion rdg0n ⊢ ¬ A ∈ V → rec ⁡ F A ⁡ ∅ = ∅

Proof

Step Hyp Ref Expression
1 0elon ⊢ ∅ ∈ On
2 df-rdg ⊢ rec ⁡ F A = recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
3 2 tfr2 ⊢ ∅ ∈ On → rec ⁡ F A ⁡ ∅ = g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ rec ⁡ F A ↾ ∅
4 1 3 ax-mp ⊢ rec ⁡ F A ⁡ ∅ = g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ rec ⁡ F A ↾ ∅
5 res0 ⊢ rec ⁡ F A ↾ ∅ = ∅
6 5 fveq2i ⊢ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ rec ⁡ F A ↾ ∅ = g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ ∅
7 4 6 eqtri ⊢ rec ⁡ F A ⁡ ∅ = g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ ∅
8 iftrue ⊢ g = ∅ → if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = A
9 eqid ⊢ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
10 8 9 fvmptn ⊢ ¬ A ∈ V → g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ ∅ = ∅
11 7 10 eqtrid ⊢ ¬ A ∈ V → rec ⁡ F A ⁡ ∅ = ∅