Theorem funimass4f

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017)

	Ref	Expression
Hypotheses	funimass4f.1	⊢ Ⅎ 𝑥 𝐴
	funimass4f.2	⊢ Ⅎ 𝑥 𝐵
	funimass4f.3	⊢ Ⅎ 𝑥 𝐹
Assertion	funimass4f	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		funimass4f.1	⊢ Ⅎ 𝑥 𝐴
2		funimass4f.2	⊢ Ⅎ 𝑥 𝐵
3		funimass4f.3	⊢ Ⅎ 𝑥 𝐹
4	3	nffun	⊢ Ⅎ 𝑥 Fun 𝐹
5	3	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
6	1 5	nfss	⊢ Ⅎ 𝑥 𝐴 ⊆ dom 𝐹
7	4 6	nfan	⊢ Ⅎ 𝑥 ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 )
8	3 1	nfima	⊢ Ⅎ 𝑥 ( 𝐹 “ 𝐴 )
9	8 2	nfss	⊢ Ⅎ 𝑥 ( 𝐹 “ 𝐴 ) ⊆ 𝐵
10	7 9	nfan	⊢ Ⅎ 𝑥 ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝐵 )
11		funfvima2	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) ) )
12		ssel	⊢ ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
13	11 12	sylan9	⊢ ( ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
14	10 13	ralrimi	⊢ ( ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
15	1 3	dfimafnf	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )
16	15	adantr	⊢ ( ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )
17	2	abrexss	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } ⊆ 𝐵 )
18	17	adantl	⊢ ( ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } ⊆ 𝐵 )
19	16 18	eqsstrd	⊢ ( ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 )
20	14 19	impbida	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )