Metamath Proof Explorer


Theorem rdgprc

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

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

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑧 = ∅ → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , 𝐼 ) ‘ ∅ ) )
2 fveq2 ( 𝑧 = ∅ → ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ ∅ ) )
3 1 2 eqeq12d ( 𝑧 = ∅ → ( ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ↔ ( rec ( 𝐹 , 𝐼 ) ‘ ∅ ) = ( rec ( 𝐹 , ∅ ) ‘ ∅ ) ) )
4 3 imbi2d ( 𝑧 = ∅ → ( ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ) ↔ ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ ∅ ) = ( rec ( 𝐹 , ∅ ) ‘ ∅ ) ) ) )
5 fveq2 ( 𝑧 = 𝑦 → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) )
6 fveq2 ( 𝑧 = 𝑦 → ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) )
7 5 6 eqeq12d ( 𝑧 = 𝑦 → ( ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ↔ ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) )
8 7 imbi2d ( 𝑧 = 𝑦 → ( ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ) ↔ ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) ) )
9 fveq2 ( 𝑧 = suc 𝑦 → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , 𝐼 ) ‘ suc 𝑦 ) )
10 fveq2 ( 𝑧 = suc 𝑦 → ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ suc 𝑦 ) )
11 9 10 eqeq12d ( 𝑧 = suc 𝑦 → ( ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ↔ ( rec ( 𝐹 , 𝐼 ) ‘ suc 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ suc 𝑦 ) ) )
12 11 imbi2d ( 𝑧 = suc 𝑦 → ( ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ) ↔ ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ suc 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ suc 𝑦 ) ) ) )
13 fveq2 ( 𝑧 = 𝑥 → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , 𝐼 ) ‘ 𝑥 ) )
14 fveq2 ( 𝑧 = 𝑥 → ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑥 ) )
15 13 14 eqeq12d ( 𝑧 = 𝑥 → ( ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ↔ ( rec ( 𝐹 , 𝐼 ) ‘ 𝑥 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑥 ) ) )
16 15 imbi2d ( 𝑧 = 𝑥 → ( ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ) ↔ ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑥 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑥 ) ) ) )
17 rdgprc0 ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ ∅ ) = ∅ )
18 0ex ∅ ∈ V
19 18 rdg0 ( rec ( 𝐹 , ∅ ) ‘ ∅ ) = ∅
20 17 19 eqtr4di ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ ∅ ) = ( rec ( 𝐹 , ∅ ) ‘ ∅ ) )
21 fveq2 ( ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) → ( 𝐹 ‘ ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) ) = ( 𝐹 ‘ ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) )
22 rdgsuc ( 𝑦 ∈ On → ( rec ( 𝐹 , 𝐼 ) ‘ suc 𝑦 ) = ( 𝐹 ‘ ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) ) )
23 rdgsuc ( 𝑦 ∈ On → ( rec ( 𝐹 , ∅ ) ‘ suc 𝑦 ) = ( 𝐹 ‘ ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) )
24 22 23 eqeq12d ( 𝑦 ∈ On → ( ( rec ( 𝐹 , 𝐼 ) ‘ suc 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ suc 𝑦 ) ↔ ( 𝐹 ‘ ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) ) = ( 𝐹 ‘ ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) ) )
25 21 24 syl5ibr ( 𝑦 ∈ On → ( ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) → ( rec ( 𝐹 , 𝐼 ) ‘ suc 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ suc 𝑦 ) ) )
26 25 imim2d ( 𝑦 ∈ On → ( ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) → ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ suc 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ suc 𝑦 ) ) ) )
27 r19.21v ( ∀ 𝑦𝑧 ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) ↔ ( ¬ 𝐼 ∈ V → ∀ 𝑦𝑧 ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) )
28 limord ( Lim 𝑧 → Ord 𝑧 )
29 ordsson ( Ord 𝑧𝑧 ⊆ On )
30 rdgfnon rec ( 𝐹 , 𝐼 ) Fn On
31 rdgfnon rec ( 𝐹 , ∅ ) Fn On
32 fvreseq ( ( ( rec ( 𝐹 , 𝐼 ) Fn On ∧ rec ( 𝐹 , ∅ ) Fn On ) ∧ 𝑧 ⊆ On ) → ( ( rec ( 𝐹 , 𝐼 ) ↾ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ↾ 𝑧 ) ↔ ∀ 𝑦𝑧 ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) )
33 30 31 32 mpanl12 ( 𝑧 ⊆ On → ( ( rec ( 𝐹 , 𝐼 ) ↾ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ↾ 𝑧 ) ↔ ∀ 𝑦𝑧 ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) )
34 28 29 33 3syl ( Lim 𝑧 → ( ( rec ( 𝐹 , 𝐼 ) ↾ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ↾ 𝑧 ) ↔ ∀ 𝑦𝑧 ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) )
35 rneq ( ( rec ( 𝐹 , 𝐼 ) ↾ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ↾ 𝑧 ) → ran ( rec ( 𝐹 , 𝐼 ) ↾ 𝑧 ) = ran ( rec ( 𝐹 , ∅ ) ↾ 𝑧 ) )
36 df-ima ( rec ( 𝐹 , 𝐼 ) “ 𝑧 ) = ran ( rec ( 𝐹 , 𝐼 ) ↾ 𝑧 )
37 df-ima ( rec ( 𝐹 , ∅ ) “ 𝑧 ) = ran ( rec ( 𝐹 , ∅ ) ↾ 𝑧 )
38 35 36 37 3eqtr4g ( ( rec ( 𝐹 , 𝐼 ) ↾ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ↾ 𝑧 ) → ( rec ( 𝐹 , 𝐼 ) “ 𝑧 ) = ( rec ( 𝐹 , ∅ ) “ 𝑧 ) )
39 38 unieqd ( ( rec ( 𝐹 , 𝐼 ) ↾ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ↾ 𝑧 ) → ( rec ( 𝐹 , 𝐼 ) “ 𝑧 ) = ( rec ( 𝐹 , ∅ ) “ 𝑧 ) )
40 vex 𝑧 ∈ V
41 rdglim ( ( 𝑧 ∈ V ∧ Lim 𝑧 ) → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , 𝐼 ) “ 𝑧 ) )
42 rdglim ( ( 𝑧 ∈ V ∧ Lim 𝑧 ) → ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) “ 𝑧 ) )
43 41 42 eqeq12d ( ( 𝑧 ∈ V ∧ Lim 𝑧 ) → ( ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ↔ ( rec ( 𝐹 , 𝐼 ) “ 𝑧 ) = ( rec ( 𝐹 , ∅ ) “ 𝑧 ) ) )
44 40 43 mpan ( Lim 𝑧 → ( ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ↔ ( rec ( 𝐹 , 𝐼 ) “ 𝑧 ) = ( rec ( 𝐹 , ∅ ) “ 𝑧 ) ) )
45 39 44 syl5ibr ( Lim 𝑧 → ( ( rec ( 𝐹 , 𝐼 ) ↾ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ↾ 𝑧 ) → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ) )
46 34 45 sylbird ( Lim 𝑧 → ( ∀ 𝑦𝑧 ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ) )
47 46 imim2d ( Lim 𝑧 → ( ( ¬ 𝐼 ∈ V → ∀ 𝑦𝑧 ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) → ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ) ) )
48 27 47 syl5bi ( Lim 𝑧 → ( ∀ 𝑦𝑧 ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑦 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑦 ) ) → ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑧 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑧 ) ) ) )
49 4 8 12 16 20 26 48 tfinds ( 𝑥 ∈ On → ( ¬ 𝐼 ∈ V → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑥 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑥 ) ) )
50 49 com12 ( ¬ 𝐼 ∈ V → ( 𝑥 ∈ On → ( rec ( 𝐹 , 𝐼 ) ‘ 𝑥 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑥 ) ) )
51 50 ralrimiv ( ¬ 𝐼 ∈ V → ∀ 𝑥 ∈ On ( rec ( 𝐹 , 𝐼 ) ‘ 𝑥 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑥 ) )
52 eqfnfv ( ( rec ( 𝐹 , 𝐼 ) Fn On ∧ rec ( 𝐹 , ∅ ) Fn On ) → ( rec ( 𝐹 , 𝐼 ) = rec ( 𝐹 , ∅ ) ↔ ∀ 𝑥 ∈ On ( rec ( 𝐹 , 𝐼 ) ‘ 𝑥 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑥 ) ) )
53 30 31 52 mp2an ( rec ( 𝐹 , 𝐼 ) = rec ( 𝐹 , ∅ ) ↔ ∀ 𝑥 ∈ On ( rec ( 𝐹 , 𝐼 ) ‘ 𝑥 ) = ( rec ( 𝐹 , ∅ ) ‘ 𝑥 ) )
54 51 53 sylibr ( ¬ 𝐼 ∈ V → rec ( 𝐹 , 𝐼 ) = rec ( 𝐹 , ∅ ) )