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