Theorem intimag

Description: Requirement for the image under the intersection of relations to equal the intersection of the images of those relations. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	intimag	⊢ ( ∀ 𝑦 ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) → ( ∩ 𝐴 “ 𝐵 ) = ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } )

Proof

Step	Hyp	Ref	Expression
1		r19.12	⊢ ( ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
2		id	⊢ ( ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) → ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
3	1 2	impbid2	⊢ ( ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) → ( ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
4		elimaint	⊢ ( 𝑦 ∈ ( ∩ 𝐴 “ 𝐵 ) ↔ ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
5		elintima	⊢ ( 𝑦 ∈ ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
6	3 4 5	3bitr4g	⊢ ( ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) → ( 𝑦 ∈ ( ∩ 𝐴 “ 𝐵 ) ↔ 𝑦 ∈ ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } ) )
7	6	alimi	⊢ ( ∀ 𝑦 ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) → ∀ 𝑦 ( 𝑦 ∈ ( ∩ 𝐴 “ 𝐵 ) ↔ 𝑦 ∈ ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } ) )
8		dfcleq	⊢ ( ( ∩ 𝐴 “ 𝐵 ) = ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } ↔ ∀ 𝑦 ( 𝑦 ∈ ( ∩ 𝐴 “ 𝐵 ) ↔ 𝑦 ∈ ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } ) )
9	7 8	sylibr	⊢ ( ∀ 𝑦 ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 → ∃ 𝑏 ∈ 𝐵 ∀ 𝑎 ∈ 𝐴 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) → ( ∩ 𝐴 “ 𝐵 ) = ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } )