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

Metamath Proof Explorer

Theorem wess

Description: Subset theorem for the well-ordering predicate. Exercise 4 of TakeutiZaring p. 31. (Contributed by NM, 19-Apr-1994)

Ref Expression
Assertion wess ⊢ A ⊆ B → R We B → R We A

Proof

Step Hyp Ref Expression
1 frss ⊢ A ⊆ B → R Fr B → R Fr A
2 soss ⊢ A ⊆ B → R Or B → R Or A
3 1 2 anim12d ⊢ A ⊆ B → R Fr B ∧ R Or B → R Fr A ∧ R Or A
4 df-we ⊢ R We B ↔ R Fr B ∧ R Or B
5 df-we ⊢ R We A ↔ R Fr A ∧ R Or A
6 3 4 5 3imtr4g ⊢ A ⊆ B → R We B → R We A