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

Metamath Proof Explorer

Theorem resco

Description: Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006)

Ref Expression
Assertion resco ( ( 𝐴 ∘ 𝐵 ) ↾ 𝐶 ) = ( 𝐴 ∘ ( 𝐵 ↾ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ( ( 𝐴 ∘ 𝐵 ) ↾ 𝐶 )
2 relco ⊢ Rel ( 𝐴 ∘ ( 𝐵 ↾ 𝐶 ) )
3 vex ⊢ 𝑥 ∈ V
4 vex ⊢ 𝑦 ∈ V
5 3 4 brco ⊢ ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ↔ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
6 5 anbi2i ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ) ↔ ( 𝑥 ∈ 𝐶 ∧ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
7 19.42v ⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝐶 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐶 ∧ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
8 vex ⊢ 𝑧 ∈ V
9 8 brresi ⊢ ( 𝑥 ( 𝐵 ↾ 𝐶 ) 𝑧 ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐵 𝑧 ) )
10 9 anbi1i ⊢ ( ( 𝑥 ( 𝐵 ↾ 𝐶 ) 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐵 𝑧 ) ∧ 𝑧 𝐴 𝑦 ) )
11 anass ⊢ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐵 𝑧 ) ∧ 𝑧 𝐴 𝑦 ) ↔ ( 𝑥 ∈ 𝐶 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
12 10 11 bitr2i ⊢ ( ( 𝑥 ∈ 𝐶 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) ↔ ( 𝑥 ( 𝐵 ↾ 𝐶 ) 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
13 12 exbii ⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝐶 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) ↔ ∃ 𝑧 ( 𝑥 ( 𝐵 ↾ 𝐶 ) 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
14 6 7 13 3bitr2i ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ) ↔ ∃ 𝑧 ( 𝑥 ( 𝐵 ↾ 𝐶 ) 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
15 4 brresi ⊢ ( 𝑥 ( ( 𝐴 ∘ 𝐵 ) ↾ 𝐶 ) 𝑦 ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ) )
16 3 4 brco ⊢ ( 𝑥 ( 𝐴 ∘ ( 𝐵 ↾ 𝐶 ) ) 𝑦 ↔ ∃ 𝑧 ( 𝑥 ( 𝐵 ↾ 𝐶 ) 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
17 14 15 16 3bitr4i ⊢ ( 𝑥 ( ( 𝐴 ∘ 𝐵 ) ↾ 𝐶 ) 𝑦 ↔ 𝑥 ( 𝐴 ∘ ( 𝐵 ↾ 𝐶 ) ) 𝑦 )
18 1 2 17 eqbrriv ⊢ ( ( 𝐴 ∘ 𝐵 ) ↾ 𝐶 ) = ( 𝐴 ∘ ( 𝐵 ↾ 𝐶 ) )