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