Step |
Hyp |
Ref |
Expression |
1 |
|
df-ima |
⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 ) |
2 |
|
resfunexg |
⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 ↾ 𝐴 ) ∈ V ) |
3 |
2
|
dmexd |
⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝐵 ) → dom ( 𝐹 ↾ 𝐴 ) ∈ V ) |
4 |
|
funres |
⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐴 ) ) |
5 |
|
funforn |
⊢ ( Fun ( 𝐹 ↾ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) ) |
6 |
4 5
|
sylib |
⊢ ( Fun 𝐹 → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) ) |
7 |
6
|
adantr |
⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) ) |
8 |
|
fodomg |
⊢ ( dom ( 𝐹 ↾ 𝐴 ) ∈ V → ( ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) → ran ( 𝐹 ↾ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) ) ) |
9 |
3 7 8
|
sylc |
⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝐵 ) → ran ( 𝐹 ↾ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) ) |
10 |
1 9
|
eqbrtrid |
⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 “ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) ) |
11 |
10
|
expcom |
⊢ ( 𝐴 ∈ 𝐵 → ( Fun 𝐹 → ( 𝐹 “ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) ) ) |
12 |
|
dmres |
⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 ) |
13 |
|
inss1 |
⊢ ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴 |
14 |
12 13
|
eqsstri |
⊢ dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 |
15 |
|
ssdomg |
⊢ ( 𝐴 ∈ 𝐵 → ( dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 → dom ( 𝐹 ↾ 𝐴 ) ≼ 𝐴 ) ) |
16 |
14 15
|
mpi |
⊢ ( 𝐴 ∈ 𝐵 → dom ( 𝐹 ↾ 𝐴 ) ≼ 𝐴 ) |
17 |
|
domtr |
⊢ ( ( ( 𝐹 “ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) ≼ 𝐴 ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) |
18 |
16 17
|
sylan2 |
⊢ ( ( ( 𝐹 “ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) |
19 |
18
|
expcom |
⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 “ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) ) |
20 |
11 19
|
syld |
⊢ ( 𝐴 ∈ 𝐵 → ( Fun 𝐹 → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) ) |