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

Metamath Proof Explorer

Theorem ressabs

Description: Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Assertion ressabs ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ssexg ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑋 ) → 𝐵 ∈ V )
2 1 ancoms ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ V )
3 ressress ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
4 2 3 syldan ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
5 simpr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ⊆ 𝐴 )
6 sseqin2 ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐵 )
7 5 6 sylib ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) = 𝐵 )
8 7 oveq2d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ( 𝑊 ↾s 𝐵 ) )
9 4 8 eqtrd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s 𝐵 ) )