| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0elon 6438 | . . . 4
⊢ ∅
∈ On | 
| 2 |  | rdgval 8460 | . . . 4
⊢ (∅
∈ On → (rec(𝐹,
𝐼)‘∅) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(rec(𝐹, 𝐼) ↾ ∅))) | 
| 3 | 1, 2 | ax-mp 5 | . . 3
⊢
(rec(𝐹, 𝐼)‘∅) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(rec(𝐹, 𝐼) ↾ ∅)) | 
| 4 |  | res0 6001 | . . . 4
⊢
(rec(𝐹, 𝐼) ↾ ∅) =
∅ | 
| 5 | 4 | fveq2i 6909 | . . 3
⊢ ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(rec(𝐹, 𝐼) ↾ ∅)) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘∅) | 
| 6 | 3, 5 | eqtri 2765 | . 2
⊢
(rec(𝐹, 𝐼)‘∅) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘∅) | 
| 7 |  | eqeq1 2741 | . . . . . . 7
⊢ (𝑔 = ∅ → (𝑔 = ∅ ↔ ∅ =
∅)) | 
| 8 |  | dmeq 5914 | . . . . . . . . 9
⊢ (𝑔 = ∅ → dom 𝑔 = dom ∅) | 
| 9 |  | limeq 6396 | . . . . . . . . 9
⊢ (dom
𝑔 = dom ∅ → (Lim
dom 𝑔 ↔ Lim dom
∅)) | 
| 10 | 8, 9 | syl 17 | . . . . . . . 8
⊢ (𝑔 = ∅ → (Lim dom 𝑔 ↔ Lim dom
∅)) | 
| 11 |  | rneq 5947 | . . . . . . . . 9
⊢ (𝑔 = ∅ → ran 𝑔 = ran ∅) | 
| 12 | 11 | unieqd 4920 | . . . . . . . 8
⊢ (𝑔 = ∅ → ∪ ran 𝑔 = ∪ ran
∅) | 
| 13 |  | id 22 | . . . . . . . . . 10
⊢ (𝑔 = ∅ → 𝑔 = ∅) | 
| 14 | 8 | unieqd 4920 | . . . . . . . . . 10
⊢ (𝑔 = ∅ → ∪ dom 𝑔 = ∪ dom
∅) | 
| 15 | 13, 14 | fveq12d 6913 | . . . . . . . . 9
⊢ (𝑔 = ∅ → (𝑔‘∪ dom 𝑔) = (∅‘∪ dom ∅)) | 
| 16 | 15 | fveq2d 6910 | . . . . . . . 8
⊢ (𝑔 = ∅ → (𝐹‘(𝑔‘∪ dom 𝑔)) = (𝐹‘(∅‘∪ dom ∅))) | 
| 17 | 10, 12, 16 | ifbieq12d 4554 | . . . . . . 7
⊢ (𝑔 = ∅ → if(Lim dom
𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))) = if(Lim dom ∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) | 
| 18 | 7, 17 | ifbieq2d 4552 | . . . . . 6
⊢ (𝑔 = ∅ → if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))) = if(∅ = ∅,
𝐼, if(Lim dom ∅,
∪ ran ∅, (𝐹‘(∅‘∪ dom ∅))))) | 
| 19 | 18 | eleq1d 2826 | . . . . 5
⊢ (𝑔 = ∅ → (if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))) ∈ V ↔ if(∅
= ∅, 𝐼, if(Lim dom
∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) ∈ V)) | 
| 20 |  | eqid 2737 | . . . . . 6
⊢ (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) = (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) | 
| 21 | 20 | dmmpt 6260 | . . . . 5
⊢ dom
(𝑔 ∈ V ↦
if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) = {𝑔 ∈ V ∣ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))) ∈ V} | 
| 22 | 19, 21 | elrab2 3695 | . . . 4
⊢ (∅
∈ dom (𝑔 ∈ V
↦ if(𝑔 = ∅,
𝐼, if(Lim dom 𝑔, ∪
ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) ↔ (∅ ∈ V
∧ if(∅ = ∅, 𝐼, if(Lim dom ∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) ∈ V)) | 
| 23 |  | eqid 2737 | . . . . . . 7
⊢ ∅ =
∅ | 
| 24 | 23 | iftruei 4532 | . . . . . 6
⊢
if(∅ = ∅, 𝐼, if(Lim dom ∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) = 𝐼 | 
| 25 | 24 | eleq1i 2832 | . . . . 5
⊢
(if(∅ = ∅, 𝐼, if(Lim dom ∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) ∈ V ↔ 𝐼 ∈ V) | 
| 26 | 25 | biimpi 216 | . . . 4
⊢
(if(∅ = ∅, 𝐼, if(Lim dom ∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) ∈ V → 𝐼 ∈ V) | 
| 27 | 22, 26 | simplbiim 504 | . . 3
⊢ (∅
∈ dom (𝑔 ∈ V
↦ if(𝑔 = ∅,
𝐼, if(Lim dom 𝑔, ∪
ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) → 𝐼 ∈ V) | 
| 28 |  | ndmfv 6941 | . . 3
⊢ (¬
∅ ∈ dom (𝑔
∈ V ↦ if(𝑔 =
∅, 𝐼, if(Lim dom
𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘∅) =
∅) | 
| 29 | 27, 28 | nsyl5 159 | . 2
⊢ (¬
𝐼 ∈ V → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘∅) =
∅) | 
| 30 | 6, 29 | eqtrid 2789 | 1
⊢ (¬
𝐼 ∈ V →
(rec(𝐹, 𝐼)‘∅) = ∅) |