Step |
Hyp |
Ref |
Expression |
1 |
|
ordtypelem.1 |
⊢ 𝐹 = recs ( 𝐺 ) |
2 |
|
ordtypelem.2 |
⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 } |
3 |
|
ordtypelem.3 |
⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) ) |
4 |
|
ordtypelem.5 |
⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } |
5 |
|
ordtypelem.6 |
⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 ) |
6 |
|
ordtypelem.7 |
⊢ ( 𝜑 → 𝑅 We 𝐴 ) |
7 |
|
ordtypelem.8 |
⊢ ( 𝜑 → 𝑅 Se 𝐴 ) |
8 |
1 2 3 4 5 6 7
|
ordtypelem2 |
⊢ ( 𝜑 → Ord 𝑇 ) |
9 |
1
|
tfr1a |
⊢ ( Fun 𝐹 ∧ Lim dom 𝐹 ) |
10 |
9
|
simpri |
⊢ Lim dom 𝐹 |
11 |
|
limord |
⊢ ( Lim dom 𝐹 → Ord dom 𝐹 ) |
12 |
10 11
|
ax-mp |
⊢ Ord dom 𝐹 |
13 |
|
ordin |
⊢ ( ( Ord 𝑇 ∧ Ord dom 𝐹 ) → Ord ( 𝑇 ∩ dom 𝐹 ) ) |
14 |
8 12 13
|
sylancl |
⊢ ( 𝜑 → Ord ( 𝑇 ∩ dom 𝐹 ) ) |
15 |
1 2 3 4 5 6 7
|
ordtypelem4 |
⊢ ( 𝜑 → 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 ) |
16 |
15
|
fdmd |
⊢ ( 𝜑 → dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) ) |
17 |
|
ordeq |
⊢ ( dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) → ( Ord dom 𝑂 ↔ Ord ( 𝑇 ∩ dom 𝐹 ) ) ) |
18 |
16 17
|
syl |
⊢ ( 𝜑 → ( Ord dom 𝑂 ↔ Ord ( 𝑇 ∩ dom 𝐹 ) ) ) |
19 |
14 18
|
mpbird |
⊢ ( 𝜑 → Ord dom 𝑂 ) |
20 |
15
|
ffdmd |
⊢ ( 𝜑 → 𝑂 : dom 𝑂 ⟶ 𝐴 ) |
21 |
19 20
|
jca |
⊢ ( 𝜑 → ( Ord dom 𝑂 ∧ 𝑂 : dom 𝑂 ⟶ 𝐴 ) ) |