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

Metamath Proof Explorer

Theorem elimampt

Description: Membership in the image of a mapping. (Contributed by Thierry Arnoux, 3-Jan-2022)

Ref Expression
Hypotheses elimampt.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
elimampt.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
elimampt.d ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
Assertion elimampt ( 𝜑 → ( 𝐶 ∈ ( 𝐹 “ 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐷 𝐶 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elimampt.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2 elimampt.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
3 elimampt.d ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
4 df-ima ⊢ ( 𝐹 “ 𝐷 ) = ran ( 𝐹 ↾ 𝐷 )
5 4 eleq2i ⊢ ( 𝐶 ∈ ( 𝐹 “ 𝐷 ) ↔ 𝐶 ∈ ran ( 𝐹 ↾ 𝐷 ) )
6 1 reseq1i ⊢ ( 𝐹 ↾ 𝐷 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐷 )
7 resmpt ⊢ ( 𝐷 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) )
8 6 7 eqtrid ⊢ ( 𝐷 ⊆ 𝐴 → ( 𝐹 ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) )
9 8 rneqd ⊢ ( 𝐷 ⊆ 𝐴 → ran ( 𝐹 ↾ 𝐷 ) = ran ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) )
10 9 eleq2d ⊢ ( 𝐷 ⊆ 𝐴 → ( 𝐶 ∈ ran ( 𝐹 ↾ 𝐷 ) ↔ 𝐶 ∈ ran ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ) )
11 3 10 syl ⊢ ( 𝜑 → ( 𝐶 ∈ ran ( 𝐹 ↾ 𝐷 ) ↔ 𝐶 ∈ ran ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ) )
12 eqid ⊢ ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
13 12 elrnmpt ⊢ ( 𝐶 ∈ 𝑊 → ( 𝐶 ∈ ran ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐷 𝐶 = 𝐵 ) )
14 2 13 syl ⊢ ( 𝜑 → ( 𝐶 ∈ ran ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐷 𝐶 = 𝐵 ) )
15 11 14 bitrd ⊢ ( 𝜑 → ( 𝐶 ∈ ran ( 𝐹 ↾ 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐷 𝐶 = 𝐵 ) )
16 5 15 bitrid ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 “ 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐷 𝐶 = 𝐵 ) )