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

Metamath Proof Explorer

Theorem imassmpt

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses imassmpt.1 ⊢ Ⅎ 𝑥 𝜑
imassmpt.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐵 ∈ 𝑉 )
imassmpt.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion imassmpt ( 𝜑 → ( ( 𝐹 “ 𝐶 ) ⊆ 𝐷 ↔ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) 𝐵 ∈ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 imassmpt.1 ⊢ Ⅎ 𝑥 𝜑
2 imassmpt.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐵 ∈ 𝑉 )
3 imassmpt.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4 df-ima ⊢ ( 𝐹 “ 𝐶 ) = ran ( 𝐹 ↾ 𝐶 )
5 3 reseq1i ⊢ ( 𝐹 ↾ 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 )
6 resmpt3 ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
7 5 6 eqtri ⊢ ( 𝐹 ↾ 𝐶 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
8 7 rneqi ⊢ ran ( 𝐹 ↾ 𝐶 ) = ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
9 4 8 eqtri ⊢ ( 𝐹 “ 𝐶 ) = ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
10 9 sseq1i ⊢ ( ( 𝐹 “ 𝐶 ) ⊆ 𝐷 ↔ ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 ) ⊆ 𝐷 )
11 eqid ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 )
12 1 11 2 rnmptssbi ⊢ ( 𝜑 → ( ran ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ 𝐵 ) ⊆ 𝐷 ↔ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) 𝐵 ∈ 𝐷 ) )
13 10 12 bitrid ⊢ ( 𝜑 → ( ( 𝐹 “ 𝐶 ) ⊆ 𝐷 ↔ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) 𝐵 ∈ 𝐷 ) )