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