Metamath Proof Explorer


Theorem rdgprc0

Description: The value of the recursive definition generator at (/) when the base value is a proper class. (Contributed by Scott Fenton, 26-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion rdgprc0 ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ ∅ ) = ∅ )

Proof

Step Hyp Ref Expression
1 0elon ∅ ∈ On
2 rdgval ( ∅ ∈ On → ( rec ( 𝐹 , 𝐼 ) ‘ ∅ ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐼 ) ↾ ∅ ) ) )
3 1 2 ax-mp ( rec ( 𝐹 , 𝐼 ) ‘ ∅ ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐼 ) ↾ ∅ ) )
4 res0 ( rec ( 𝐹 , 𝐼 ) ↾ ∅ ) = ∅
5 4 fveq2i ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐼 ) ↾ ∅ ) ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) ‘ ∅ )
6 3 5 eqtri ( rec ( 𝐹 , 𝐼 ) ‘ ∅ ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) ‘ ∅ )
7 eqeq1 ( 𝑔 = ∅ → ( 𝑔 = ∅ ↔ ∅ = ∅ ) )
8 dmeq ( 𝑔 = ∅ → dom 𝑔 = dom ∅ )
9 limeq ( dom 𝑔 = dom ∅ → ( Lim dom 𝑔 ↔ Lim dom ∅ ) )
10 8 9 syl ( 𝑔 = ∅ → ( Lim dom 𝑔 ↔ Lim dom ∅ ) )
11 rneq ( 𝑔 = ∅ → ran 𝑔 = ran ∅ )
12 11 unieqd ( 𝑔 = ∅ → ran 𝑔 = ran ∅ )
13 id ( 𝑔 = ∅ → 𝑔 = ∅ )
14 8 unieqd ( 𝑔 = ∅ → dom 𝑔 = dom ∅ )
15 13 14 fveq12d ( 𝑔 = ∅ → ( 𝑔 dom 𝑔 ) = ( ∅ ‘ dom ∅ ) )
16 15 fveq2d ( 𝑔 = ∅ → ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) = ( 𝐹 ‘ ( ∅ ‘ dom ∅ ) ) )
17 10 12 16 ifbieq12d ( 𝑔 = ∅ → if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) = if ( Lim dom ∅ , ran ∅ , ( 𝐹 ‘ ( ∅ ‘ dom ∅ ) ) ) )
18 7 17 ifbieq2d ( 𝑔 = ∅ → if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) = if ( ∅ = ∅ , 𝐼 , if ( Lim dom ∅ , ran ∅ , ( 𝐹 ‘ ( ∅ ‘ dom ∅ ) ) ) ) )
19 18 eleq1d ( 𝑔 = ∅ → ( if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ∈ V ↔ if ( ∅ = ∅ , 𝐼 , if ( Lim dom ∅ , ran ∅ , ( 𝐹 ‘ ( ∅ ‘ dom ∅ ) ) ) ) ∈ V ) )
20 eqid ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) = ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) )
21 20 dmmpt dom ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) = { 𝑔 ∈ V ∣ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ∈ V }
22 19 21 elrab2 ( ∅ ∈ dom ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) ↔ ( ∅ ∈ V ∧ if ( ∅ = ∅ , 𝐼 , if ( Lim dom ∅ , ran ∅ , ( 𝐹 ‘ ( ∅ ‘ dom ∅ ) ) ) ) ∈ V ) )
23 eqid ∅ = ∅
24 23 iftruei if ( ∅ = ∅ , 𝐼 , if ( Lim dom ∅ , ran ∅ , ( 𝐹 ‘ ( ∅ ‘ dom ∅ ) ) ) ) = 𝐼
25 24 eleq1i ( if ( ∅ = ∅ , 𝐼 , if ( Lim dom ∅ , ran ∅ , ( 𝐹 ‘ ( ∅ ‘ dom ∅ ) ) ) ) ∈ V ↔ 𝐼 ∈ V )
26 25 biimpi ( if ( ∅ = ∅ , 𝐼 , if ( Lim dom ∅ , ran ∅ , ( 𝐹 ‘ ( ∅ ‘ dom ∅ ) ) ) ) ∈ V → 𝐼 ∈ V )
27 22 26 simplbiim ( ∅ ∈ dom ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) → 𝐼 ∈ V )
28 ndmfv ( ¬ ∅ ∈ dom ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) → ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) ‘ ∅ ) = ∅ )
29 27 28 nsyl5 ( ¬ 𝐼 ∈ V → ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ran 𝑔 , ( 𝐹 ‘ ( 𝑔 dom 𝑔 ) ) ) ) ) ‘ ∅ ) = ∅ )
30 6 29 syl5eq ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ ∅ ) = ∅ )