Theorem cores

Description: Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	cores	⊢ ( ran 𝐵 ⊆ 𝐶 → ( ( 𝐴 ↾ 𝐶 ) ∘ 𝐵 ) = ( 𝐴 ∘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑧 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	brelrn	⊢ ( 𝑧 𝐵 𝑦 → 𝑦 ∈ ran 𝐵 )
4		ssel	⊢ ( ran 𝐵 ⊆ 𝐶 → ( 𝑦 ∈ ran 𝐵 → 𝑦 ∈ 𝐶 ) )
5		vex	⊢ 𝑥 ∈ V
6	5	brresi	⊢ ( 𝑦 ( 𝐴 ↾ 𝐶 ) 𝑥 ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑦 𝐴 𝑥 ) )
7	6	baib	⊢ ( 𝑦 ∈ 𝐶 → ( 𝑦 ( 𝐴 ↾ 𝐶 ) 𝑥 ↔ 𝑦 𝐴 𝑥 ) )
8	3 4 7	syl56	⊢ ( ran 𝐵 ⊆ 𝐶 → ( 𝑧 𝐵 𝑦 → ( 𝑦 ( 𝐴 ↾ 𝐶 ) 𝑥 ↔ 𝑦 𝐴 𝑥 ) ) )
9	8	pm5.32d	⊢ ( ran 𝐵 ⊆ 𝐶 → ( ( 𝑧 𝐵 𝑦 ∧ 𝑦 ( 𝐴 ↾ 𝐶 ) 𝑥 ) ↔ ( 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) ) )
10	9	exbidv	⊢ ( ran 𝐵 ⊆ 𝐶 → ( ∃ 𝑦 ( 𝑧 𝐵 𝑦 ∧ 𝑦 ( 𝐴 ↾ 𝐶 ) 𝑥 ) ↔ ∃ 𝑦 ( 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) ) )
11	10	opabbidv	⊢ ( ran 𝐵 ⊆ 𝐶 → { ⟨ 𝑧 , 𝑥 ⟩ ∣ ∃ 𝑦 ( 𝑧 𝐵 𝑦 ∧ 𝑦 ( 𝐴 ↾ 𝐶 ) 𝑥 ) } = { ⟨ 𝑧 , 𝑥 ⟩ ∣ ∃ 𝑦 ( 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) } )
12		df-co	⊢ ( ( 𝐴 ↾ 𝐶 ) ∘ 𝐵 ) = { ⟨ 𝑧 , 𝑥 ⟩ ∣ ∃ 𝑦 ( 𝑧 𝐵 𝑦 ∧ 𝑦 ( 𝐴 ↾ 𝐶 ) 𝑥 ) }
13		df-co	⊢ ( 𝐴 ∘ 𝐵 ) = { ⟨ 𝑧 , 𝑥 ⟩ ∣ ∃ 𝑦 ( 𝑧 𝐵 𝑦 ∧ 𝑦 𝐴 𝑥 ) }
14	11 12 13	3eqtr4g	⊢ ( ran 𝐵 ⊆ 𝐶 → ( ( 𝐴 ↾ 𝐶 ) ∘ 𝐵 ) = ( 𝐴 ∘ 𝐵 ) )