Theorem ressid2

Description: General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014)

	Ref	Expression
Hypotheses	ressbas.r	⊢ 𝑅 = ( 𝑊 ↾s 𝐴 )
	ressbas.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion	ressid2	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		ressbas.r	⊢ 𝑅 = ( 𝑊 ↾s 𝐴 )
2		ressbas.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
3	1 2	ressval	⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ) )
4		iftrue	⊢ ( 𝐵 ⊆ 𝐴 → if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ) = 𝑊 )
5	3 4	sylan9eqr	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) ) → 𝑅 = 𝑊 )
6	5	3impb	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = 𝑊 )