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

Metamath Proof Explorer

Theorem ressle

Description: le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015)

Ref Expression
Hypotheses ressle.1 ⊢ 𝑊 = ( 𝐾 ↾s 𝐴 )
ressle.2 ⊢ ≤ = ( le ‘ 𝐾 )
Assertion ressle ( 𝐴 ∈ 𝑉 → ≤ = ( le ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 ressle.1 ⊢ 𝑊 = ( 𝐾 ↾s 𝐴 )
2 ressle.2 ⊢ ≤ = ( le ‘ 𝐾 )
3 pleid ⊢ le = Slot ( le ‘ ndx )
4 plendxnbasendx ⊢ ( le ‘ ndx ) ≠ ( Base ‘ ndx )
5 1 2 3 4 resseqnbas ⊢ ( 𝐴 ∈ 𝑉 → ≤ = ( le ‘ 𝑊 ) )