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