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