Step | Hyp | Ref
| Expression |
1 | | 0elon 6126 |
. . . 4
⊢ ∅
∈ On |
2 | | rdgval 7915 |
. . . 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 5745 |
. . . 4
⊢
(rec(𝐹, 𝐼) ↾ ∅) =
∅ |
5 | 4 | fveq2i 6548 |
. . 3
⊢ ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(rec(𝐹, 𝐼) ↾ ∅)) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘∅) |
6 | 3, 5 | eqtri 2821 |
. 2
⊢
(rec(𝐹, 𝐼)‘∅) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘∅) |
7 | | eqeq1 2801 |
. . . . . . . 8
⊢ (𝑔 = ∅ → (𝑔 = ∅ ↔ ∅ =
∅)) |
8 | | dmeq 5665 |
. . . . . . . . . 10
⊢ (𝑔 = ∅ → dom 𝑔 = dom ∅) |
9 | | limeq 6085 |
. . . . . . . . . 10
⊢ (dom
𝑔 = dom ∅ → (Lim
dom 𝑔 ↔ Lim dom
∅)) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝑔 = ∅ → (Lim dom 𝑔 ↔ Lim dom
∅)) |
11 | | rneq 5695 |
. . . . . . . . . 10
⊢ (𝑔 = ∅ → ran 𝑔 = ran ∅) |
12 | 11 | unieqd 4761 |
. . . . . . . . 9
⊢ (𝑔 = ∅ → ∪ ran 𝑔 = ∪ ran
∅) |
13 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑔 = ∅ → 𝑔 = ∅) |
14 | 8 | unieqd 4761 |
. . . . . . . . . . 11
⊢ (𝑔 = ∅ → ∪ dom 𝑔 = ∪ dom
∅) |
15 | 13, 14 | fveq12d 6552 |
. . . . . . . . . 10
⊢ (𝑔 = ∅ → (𝑔‘∪ dom 𝑔) = (∅‘∪ dom ∅)) |
16 | 15 | fveq2d 6549 |
. . . . . . . . 9
⊢ (𝑔 = ∅ → (𝐹‘(𝑔‘∪ dom 𝑔)) = (𝐹‘(∅‘∪ dom ∅))) |
17 | 10, 12, 16 | ifbieq12d 4414 |
. . . . . . . 8
⊢ (𝑔 = ∅ → if(Lim dom
𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))) = if(Lim dom ∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) |
18 | 7, 17 | ifbieq2d 4412 |
. . . . . . 7
⊢ (𝑔 = ∅ → if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))) = if(∅ = ∅,
𝐼, if(Lim dom ∅,
∪ ran ∅, (𝐹‘(∅‘∪ dom ∅))))) |
19 | 18 | eleq1d 2869 |
. . . . . 6
⊢ (𝑔 = ∅ → (if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))) ∈ V ↔ if(∅
= ∅, 𝐼, if(Lim dom
∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) ∈ V)) |
20 | | eqid 2797 |
. . . . . . 7
⊢ (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) = (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) |
21 | 20 | dmmpt 5976 |
. . . . . 6
⊢ dom
(𝑔 ∈ V ↦
if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) = {𝑔 ∈ V ∣ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))) ∈ V} |
22 | 19, 21 | elrab2 3624 |
. . . . 5
⊢ (∅
∈ dom (𝑔 ∈ V
↦ if(𝑔 = ∅,
𝐼, if(Lim dom 𝑔, ∪
ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) ↔ (∅ ∈ V
∧ if(∅ = ∅, 𝐼, if(Lim dom ∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) ∈ V)) |
23 | | eqid 2797 |
. . . . . . . . 9
⊢ ∅ =
∅ |
24 | 23 | iftruei 4394 |
. . . . . . . 8
⊢
if(∅ = ∅, 𝐼, if(Lim dom ∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) = 𝐼 |
25 | 24 | eleq1i 2875 |
. . . . . . 7
⊢
(if(∅ = ∅, 𝐼, if(Lim dom ∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) ∈ V ↔ 𝐼 ∈ V) |
26 | 25 | biimpi 217 |
. . . . . 6
⊢
(if(∅ = ∅, 𝐼, if(Lim dom ∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) ∈ V → 𝐼 ∈ V) |
27 | 26 | adantl 482 |
. . . . 5
⊢ ((∅
∈ V ∧ if(∅ = ∅, 𝐼, if(Lim dom ∅, ∪ ran ∅, (𝐹‘(∅‘∪ dom ∅)))) ∈ V) → 𝐼 ∈ V) |
28 | 22, 27 | sylbi 218 |
. . . 4
⊢ (∅
∈ dom (𝑔 ∈ V
↦ if(𝑔 = ∅,
𝐼, if(Lim dom 𝑔, ∪
ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) → 𝐼 ∈ V) |
29 | 28 | con3i 157 |
. . 3
⊢ (¬
𝐼 ∈ V → ¬
∅ ∈ dom (𝑔
∈ V ↦ if(𝑔 =
∅, 𝐼, if(Lim dom
𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))) |
30 | | ndmfv 6575 |
. . 3
⊢ (¬
∅ ∈ dom (𝑔
∈ V ↦ if(𝑔 =
∅, 𝐼, if(Lim dom
𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘∅) =
∅) |
31 | 29, 30 | syl 17 |
. 2
⊢ (¬
𝐼 ∈ V → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘∅) =
∅) |
32 | 6, 31 | syl5eq 2845 |
1
⊢ (¬
𝐼 ∈ V →
(rec(𝐹, 𝐼)‘∅) = ∅) |