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