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

Proof

Step Hyp Ref Expression
1 0elon ⊢ ∅ ∈ On
2 rdgval ⊢ ∅ ∈ On → rec ⁡ F I ⁡ ∅ = g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ rec ⁡ F I ↾ ∅
3 1 2 ax-mp ⊢ rec ⁡ F I ⁡ ∅ = g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ rec ⁡ F I ↾ ∅
4 res0 ⊢ rec ⁡ F I ↾ ∅ = ∅
5 4 fveq2i ⊢ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ rec ⁡ F I ↾ ∅ = g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ ∅
6 3 5 eqtri ⊢ rec ⁡ F I ⁡ ∅ = g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ ∅
7 eqeq1 ⊢ g = ∅ → g = ∅ ↔ ∅ = ∅
8 dmeq ⊢ g = ∅ → dom ⁡ g = dom ⁡ ∅
9 limeq ⊢ dom ⁡ g = dom ⁡ ∅ → Lim ⁡ dom ⁡ g ↔ Lim ⁡ dom ⁡ ∅
10 8 9 syl ⊢ g = ∅ → Lim ⁡ dom ⁡ g ↔ Lim ⁡ dom ⁡ ∅
11 rneq ⊢ g = ∅ → ran ⁡ g = ran ⁡ ∅
12 11 unieqd ⊢ g = ∅ → ⋃ ran ⁡ g = ⋃ ran ⁡ ∅
13 id ⊢ g = ∅ → g = ∅
14 8 unieqd ⊢ g = ∅ → ⋃ dom ⁡ g = ⋃ dom ⁡ ∅
15 13 14 fveq12d ⊢ g = ∅ → g ⁡ ⋃ dom ⁡ g = ∅ ⁡ ⋃ dom ⁡ ∅
16 15 fveq2d ⊢ g = ∅ → F ⁡ g ⁡ ⋃ dom ⁡ g = F ⁡ ∅ ⁡ ⋃ dom ⁡ ∅
17 10 12 16 ifbieq12d ⊢ g = ∅ → if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = if Lim ⁡ dom ⁡ ∅ ⋃ ran ⁡ ∅ F ⁡ ∅ ⁡ ⋃ dom ⁡ ∅
18 7 17 ifbieq2d ⊢ g = ∅ → if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = if ∅ = ∅ I if Lim ⁡ dom ⁡ ∅ ⋃ ran ⁡ ∅ F ⁡ ∅ ⁡ ⋃ dom ⁡ ∅
19 18 eleq1d ⊢ g = ∅ → if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ∈ V ↔ if ∅ = ∅ I if Lim ⁡ dom ⁡ ∅ ⋃ ran ⁡ ∅ F ⁡ ∅ ⁡ ⋃ dom ⁡ ∅ ∈ V
20 eqid ⊢ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
21 20 dmmpt ⊢ dom ⁡ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = g ∈ V | if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ∈ V
22 19 21 elrab2 ⊢ ∅ ∈ dom ⁡ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ↔ ∅ ∈ V ∧ if ∅ = ∅ I if Lim ⁡ dom ⁡ ∅ ⋃ ran ⁡ ∅ F ⁡ ∅ ⁡ ⋃ dom ⁡ ∅ ∈ V
23 eqid ⊢ ∅ = ∅
24 23 iftruei ⊢ if ∅ = ∅ I if Lim ⁡ dom ⁡ ∅ ⋃ ran ⁡ ∅ F ⁡ ∅ ⁡ ⋃ dom ⁡ ∅ = I
25 24 eleq1i ⊢ if ∅ = ∅ I if Lim ⁡ dom ⁡ ∅ ⋃ ran ⁡ ∅ F ⁡ ∅ ⁡ ⋃ dom ⁡ ∅ ∈ V ↔ I ∈ V
26 25 biimpi ⊢ if ∅ = ∅ I if Lim ⁡ dom ⁡ ∅ ⋃ ran ⁡ ∅ F ⁡ ∅ ⁡ ⋃ dom ⁡ ∅ ∈ V → I ∈ V
27 22 26 simplbiim ⊢ ∅ ∈ dom ⁡ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g → I ∈ V
28 ndmfv ⊢ ¬ ∅ ∈ dom ⁡ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g → g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ ∅ = ∅
29 27 28 nsyl5 ⊢ ¬ I ∈ V → g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ ∅ = ∅
30 6 29 eqtrid ⊢ ¬ I ∈ V → rec ⁡ F I ⁡ ∅ = ∅