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