Step |
Hyp |
Ref |
Expression |
1 |
|
dmresv |
⊢ dom ( 𝐹 ↾ V ) = dom 𝐹 |
2 |
|
finresfin |
⊢ ( 𝐹 ∈ Fin → ( 𝐹 ↾ V ) ∈ Fin ) |
3 |
|
fvex |
⊢ ( 1st ‘ 𝑥 ) ∈ V |
4 |
|
eqid |
⊢ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) |
5 |
3 4
|
fnmpti |
⊢ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) Fn ( 𝐹 ↾ V ) |
6 |
|
dffn4 |
⊢ ( ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) Fn ( 𝐹 ↾ V ) ↔ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) ) |
7 |
5 6
|
mpbi |
⊢ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) |
8 |
|
relres |
⊢ Rel ( 𝐹 ↾ V ) |
9 |
|
reldm |
⊢ ( Rel ( 𝐹 ↾ V ) → dom ( 𝐹 ↾ V ) = ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) ) |
10 |
|
foeq3 |
⊢ ( dom ( 𝐹 ↾ V ) = ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) → ( ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ dom ( 𝐹 ↾ V ) ↔ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) ) ) |
11 |
8 9 10
|
mp2b |
⊢ ( ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ dom ( 𝐹 ↾ V ) ↔ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ ran ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) ) |
12 |
7 11
|
mpbir |
⊢ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ dom ( 𝐹 ↾ V ) |
13 |
|
fodomfi |
⊢ ( ( ( 𝐹 ↾ V ) ∈ Fin ∧ ( 𝑥 ∈ ( 𝐹 ↾ V ) ↦ ( 1st ‘ 𝑥 ) ) : ( 𝐹 ↾ V ) –onto→ dom ( 𝐹 ↾ V ) ) → dom ( 𝐹 ↾ V ) ≼ ( 𝐹 ↾ V ) ) |
14 |
2 12 13
|
sylancl |
⊢ ( 𝐹 ∈ Fin → dom ( 𝐹 ↾ V ) ≼ ( 𝐹 ↾ V ) ) |
15 |
|
resss |
⊢ ( 𝐹 ↾ V ) ⊆ 𝐹 |
16 |
|
ssdomg |
⊢ ( 𝐹 ∈ Fin → ( ( 𝐹 ↾ V ) ⊆ 𝐹 → ( 𝐹 ↾ V ) ≼ 𝐹 ) ) |
17 |
15 16
|
mpi |
⊢ ( 𝐹 ∈ Fin → ( 𝐹 ↾ V ) ≼ 𝐹 ) |
18 |
|
domtr |
⊢ ( ( dom ( 𝐹 ↾ V ) ≼ ( 𝐹 ↾ V ) ∧ ( 𝐹 ↾ V ) ≼ 𝐹 ) → dom ( 𝐹 ↾ V ) ≼ 𝐹 ) |
19 |
14 17 18
|
syl2anc |
⊢ ( 𝐹 ∈ Fin → dom ( 𝐹 ↾ V ) ≼ 𝐹 ) |
20 |
1 19
|
eqbrtrrid |
⊢ ( 𝐹 ∈ Fin → dom 𝐹 ≼ 𝐹 ) |