This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imadomg

Description: An image of a function under a set is dominated by the set. Proposition 10.34 of TakeutiZaring p. 92. (Contributed by NM, 23-Jul-2004)

Ref Expression
Assertion imadomg ( 𝐴 ∈ 𝐵 → ( Fun 𝐹 → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) )

Proof

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 𝐹 → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) )