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

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