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

Metamath Proof Explorer

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 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )