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
|
tfr1a |
⊢ ( Fun 𝐹 ∧ Lim dom 𝐹 ) |
9 |
8
|
simpli |
⊢ Fun 𝐹 |
10 |
|
funres |
⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝑇 ) ) |
11 |
9 10
|
mp1i |
⊢ ( 𝜑 → Fun ( 𝐹 ↾ 𝑇 ) ) |
12 |
11
|
funfnd |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝑇 ) Fn dom ( 𝐹 ↾ 𝑇 ) ) |
13 |
|
dmres |
⊢ dom ( 𝐹 ↾ 𝑇 ) = ( 𝑇 ∩ dom 𝐹 ) |
14 |
13
|
fneq2i |
⊢ ( ( 𝐹 ↾ 𝑇 ) Fn dom ( 𝐹 ↾ 𝑇 ) ↔ ( 𝐹 ↾ 𝑇 ) Fn ( 𝑇 ∩ dom 𝐹 ) ) |
15 |
12 14
|
sylib |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝑇 ) Fn ( 𝑇 ∩ dom 𝐹 ) ) |
16 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) |
17 |
16
|
elin1d |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → 𝑎 ∈ 𝑇 ) |
18 |
17
|
fvresd |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) ) |
19 |
|
ssrab2 |
⊢ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } ⊆ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } |
20 |
|
ssrab2 |
⊢ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ⊆ 𝐴 |
21 |
19 20
|
sstri |
⊢ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } ⊆ 𝐴 |
22 |
1 2 3 4 5 6 7
|
ordtypelem3 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } ) |
23 |
21 22
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐴 ) |
24 |
18 23
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑎 ) ∈ 𝐴 ) |
25 |
24
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑎 ) ∈ 𝐴 ) |
26 |
|
ffnfv |
⊢ ( ( 𝐹 ↾ 𝑇 ) : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 ↔ ( ( 𝐹 ↾ 𝑇 ) Fn ( 𝑇 ∩ dom 𝐹 ) ∧ ∀ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑎 ) ∈ 𝐴 ) ) |
27 |
15 25 26
|
sylanbrc |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝑇 ) : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 ) |
28 |
1 2 3 4 5 6 7
|
ordtypelem1 |
⊢ ( 𝜑 → 𝑂 = ( 𝐹 ↾ 𝑇 ) ) |
29 |
28
|
feq1d |
⊢ ( 𝜑 → ( 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 ↔ ( 𝐹 ↾ 𝑇 ) : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 ) ) |
30 |
27 29
|
mpbird |
⊢ ( 𝜑 → 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 ) |