Metamath Proof Explorer


Theorem ressval2

Description: Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014)

Ref Expression
Hypotheses ressbas.r 𝑅 = ( 𝑊s 𝐴 )
ressbas.b 𝐵 = ( Base ‘ 𝑊 )
Assertion ressval2 ( ( ¬ 𝐵𝐴𝑊𝑋𝐴𝑌 ) → 𝑅 = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴𝐵 ) ⟩ ) )

Proof

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