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 C_ B -> ( R We B -> R We A ) )

Proof

Step Hyp Ref Expression
1 frss 
 |-  ( A C_ B -> ( R Fr B -> R Fr A ) )
2 soss 
 |-  ( A C_ B -> ( R Or B -> R Or A ) )
3 1 2 anim12d 
 |-  ( A C_ 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 C_ B -> ( R We B -> R We A ) )