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 ⊢ ¬ I ∈ V → rec ⁡ F I = rec ⁡ F ∅

Proof

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