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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 )