Step |
Hyp |
Ref |
Expression |
1 |
|
tfr.1 |
⊢ 𝐹 = recs ( 𝐺 ) |
2 |
|
ordeleqon |
⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) ) |
3 |
|
eqid |
⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } |
4 |
3
|
tfrlem15 |
⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ dom recs ( 𝐺 ) ↔ ( recs ( 𝐺 ) ↾ 𝐴 ) ∈ V ) ) |
5 |
1
|
dmeqi |
⊢ dom 𝐹 = dom recs ( 𝐺 ) |
6 |
5
|
eleq2i |
⊢ ( 𝐴 ∈ dom 𝐹 ↔ 𝐴 ∈ dom recs ( 𝐺 ) ) |
7 |
1
|
reseq1i |
⊢ ( 𝐹 ↾ 𝐴 ) = ( recs ( 𝐺 ) ↾ 𝐴 ) |
8 |
7
|
eleq1i |
⊢ ( ( 𝐹 ↾ 𝐴 ) ∈ V ↔ ( recs ( 𝐺 ) ↾ 𝐴 ) ∈ V ) |
9 |
4 6 8
|
3bitr4g |
⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝐴 ) ∈ V ) ) |
10 |
|
onprc |
⊢ ¬ On ∈ V |
11 |
|
elex |
⊢ ( On ∈ dom 𝐹 → On ∈ V ) |
12 |
10 11
|
mto |
⊢ ¬ On ∈ dom 𝐹 |
13 |
|
eleq1 |
⊢ ( 𝐴 = On → ( 𝐴 ∈ dom 𝐹 ↔ On ∈ dom 𝐹 ) ) |
14 |
12 13
|
mtbiri |
⊢ ( 𝐴 = On → ¬ 𝐴 ∈ dom 𝐹 ) |
15 |
3
|
tfrlem13 |
⊢ ¬ recs ( 𝐺 ) ∈ V |
16 |
1 15
|
eqneltri |
⊢ ¬ 𝐹 ∈ V |
17 |
|
reseq2 |
⊢ ( 𝐴 = On → ( 𝐹 ↾ 𝐴 ) = ( 𝐹 ↾ On ) ) |
18 |
1
|
tfr1a |
⊢ ( Fun 𝐹 ∧ Lim dom 𝐹 ) |
19 |
18
|
simpli |
⊢ Fun 𝐹 |
20 |
|
funrel |
⊢ ( Fun 𝐹 → Rel 𝐹 ) |
21 |
19 20
|
ax-mp |
⊢ Rel 𝐹 |
22 |
18
|
simpri |
⊢ Lim dom 𝐹 |
23 |
|
limord |
⊢ ( Lim dom 𝐹 → Ord dom 𝐹 ) |
24 |
|
ordsson |
⊢ ( Ord dom 𝐹 → dom 𝐹 ⊆ On ) |
25 |
22 23 24
|
mp2b |
⊢ dom 𝐹 ⊆ On |
26 |
|
relssres |
⊢ ( ( Rel 𝐹 ∧ dom 𝐹 ⊆ On ) → ( 𝐹 ↾ On ) = 𝐹 ) |
27 |
21 25 26
|
mp2an |
⊢ ( 𝐹 ↾ On ) = 𝐹 |
28 |
17 27
|
eqtrdi |
⊢ ( 𝐴 = On → ( 𝐹 ↾ 𝐴 ) = 𝐹 ) |
29 |
28
|
eleq1d |
⊢ ( 𝐴 = On → ( ( 𝐹 ↾ 𝐴 ) ∈ V ↔ 𝐹 ∈ V ) ) |
30 |
16 29
|
mtbiri |
⊢ ( 𝐴 = On → ¬ ( 𝐹 ↾ 𝐴 ) ∈ V ) |
31 |
14 30
|
2falsed |
⊢ ( 𝐴 = On → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝐴 ) ∈ V ) ) |
32 |
9 31
|
jaoi |
⊢ ( ( 𝐴 ∈ On ∨ 𝐴 = On ) → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝐴 ) ∈ V ) ) |
33 |
2 32
|
sylbi |
⊢ ( Ord 𝐴 → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝐴 ) ∈ V ) ) |