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 ⊢ W = K ↾ 𝑠 A
ressle.2 ⊢ ≤ ˙ = ≤ K
Assertion ressle ⊢ A ∈ V → ≤ ˙ = ≤ W

Proof

Step Hyp Ref Expression
1 ressle.1 ⊢ W = K ↾ 𝑠 A
2 ressle.2 ⊢ ≤ ˙ = ≤ K
3 pleid ⊢ le = Slot ≤ ndx
4 plendxnbasendx ⊢ ≤ ndx ≠ Base ndx
5 1 2 3 4 resseqnbas ⊢ A ∈ V → ≤ ˙ = ≤ W