Theorem intimass

Description: The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	intimass	⊢ ( ∩ 𝐴 “ 𝐵 ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) }

Proof

Step	Hyp	Ref	Expression
1		r19.12	⊢ ( ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
2		elimaint	⊢ ( 𝑦 ∈ ( ∩ 𝐴 “ 𝐵 ) ↔ ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
3		elintima	⊢ ( 𝑦 ∈ ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
4	1 2 3	3imtr4i	⊢ ( 𝑦 ∈ ( ∩ 𝐴 “ 𝐵 ) → 𝑦 ∈ ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } )
5	4	ssriv	⊢ ( ∩ 𝐴 “ 𝐵 ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) }