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 imbitrrid ⊢ ( 𝑦 ∈ 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 imbitrrid ⊢ ( 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 biimtrid ⊢ ( 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 ( 𝐹 , ∅ ) )