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

Metamath Proof Explorer

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 𝐵 ⊆ 𝐶 → ( ( 𝐴 ↾ 𝐶 ) ∘ 𝐵 ) = ( 𝐴 ∘ 𝐵 ) )