Metamath Proof Explorer

Theorem funimaeq

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses funimaeq.x ⊢ Ⅎ 𝑥 𝜑
funimaeq.f ⊢ ( 𝜑 → Fun 𝐹 )
funimaeq.g ⊢ ( 𝜑 → Fun 𝐺 )
funimaeq.a ⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐹 )
funimaeq.d ⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐺 )
funimaeq.e ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
Assertion funimaeq ( 𝜑 → ( 𝐹 “ 𝐴 ) = ( 𝐺 “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 funimaeq.x ⊢ Ⅎ 𝑥 𝜑
2 funimaeq.f ⊢ ( 𝜑 → Fun 𝐹 )
3 funimaeq.g ⊢ ( 𝜑 → Fun 𝐺 )
4 funimaeq.a ⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐹 )
5 funimaeq.d ⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐺 )
6 funimaeq.e ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
7 3 funfnd ⊢ ( 𝜑 → 𝐺 Fn dom 𝐺 )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐺 Fn dom 𝐺 )
9 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ dom 𝐺 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
11 fnfvima ⊢ ( ( 𝐺 Fn dom 𝐺 ∧ 𝐴 ⊆ dom 𝐺 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) )
12 8 9 10 11 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) )
13 6 12 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) )
14 1 2 13 funimassd ⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) ⊆ ( 𝐺 “ 𝐴 ) )
15 2 funfnd ⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 Fn dom 𝐹 )
17 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ dom 𝐹 )
18 fnfvima ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) )
19 16 17 10 18 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) )
20 6 19 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) )
21 1 3 20 funimassd ⊢ ( 𝜑 → ( 𝐺 “ 𝐴 ) ⊆ ( 𝐹 “ 𝐴 ) )
22 14 21 eqssd ⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) = ( 𝐺 “ 𝐴 ) )