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 ( ¬ 𝐴 ∈ V → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = ∅ )

Proof

Step Hyp Ref Expression
1 0elon ⊢ ∅ ∈ On
2 df-rdg ⊢ rec ( 𝐹 , 𝐴 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
3 2 tfr2 ⊢ ( ∅ ∈ On → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ ∅ ) ) )
4 1 3 ax-mp ⊢ ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ ∅ ) )
5 res0 ⊢ ( rec ( 𝐹 , 𝐴 ) ↾ ∅ ) = ∅
6 5 fveq2i ⊢ ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ ∅ ) ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ∅ )
7 4 6 eqtri ⊢ ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ∅ )
8 iftrue ⊢ ( 𝑔 = ∅ → if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) = 𝐴 )
9 eqid ⊢ ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) = ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) )
10 8 9 fvmptn ⊢ ( ¬ 𝐴 ∈ V → ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ∅ ) = ∅ )
11 7 10 eqtrid ⊢ ( ¬ 𝐴 ∈ V → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = ∅ )