Metamath Proof Explorer

Theorem frss

Description: Subset theorem for the well-founded predicate. Exercise 1 of TakeutiZaring p. 31. (Contributed by NM, 3-Apr-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion frss 
|- ( A C_ B -> ( R Fr B -> R Fr A ) )

Proof

Step Hyp Ref Expression
1 sstr2 
 |-  ( x C_ A -> ( A C_ B -> x C_ B ) )
2 1 com12 
 |-  ( A C_ B -> ( x C_ A -> x C_ B ) )
3 2 anim1d 
 |-  ( A C_ B -> ( ( x C_ A /\ x =/= (/) ) -> ( x C_ B /\ x =/= (/) ) ) )
4 3 imim1d 
 |-  ( A C_ B -> ( ( ( x C_ B /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) -> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) ) )
5 4 alimdv 
 |-  ( A C_ B -> ( A. x ( ( x C_ B /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) -> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) ) )
6 df-fr 
 |-  ( R Fr B <-> A. x ( ( x C_ B /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
7 df-fr 
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
8 5 6 7 3imtr4g 
 |-  ( A C_ B -> ( R Fr B -> R Fr A ) )