Theorem funimassd

Description: Sufficient condition for the image of a function being a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	funimassd.1	⊢ Ⅎ 𝑥 𝜑
	funimassd.2	⊢ ( 𝜑 → Fun 𝐹 )
	funimassd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
Assertion	funimassd	⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		funimassd.1	⊢ Ⅎ 𝑥 𝜑
2		funimassd.2	⊢ ( 𝜑 → Fun 𝐹 )
3		funimassd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
4		fvelima	⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ ( 𝐹 “ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
5	2 4	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐹 “ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
6		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ ( 𝐹 “ 𝐴 )
7	1 6	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ( 𝐹 “ 𝐴 ) )
8		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
9		id	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( 𝐹 ‘ 𝑥 ) = 𝑦 )
10	9	eqcomd	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
11	10	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
12	3	3adant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
13	11 12	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ 𝐵 )
14	13	3exp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐵 ) ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐹 “ 𝐴 ) ) → ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐵 ) ) )
16	7 8 15	rexlimd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐹 “ 𝐴 ) ) → ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐵 ) )
17	5 16	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐹 “ 𝐴 ) ) → 𝑦 ∈ 𝐵 )
18	17	ex	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
19	18	ssrdv	⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 )