Metamath Proof Explorer

Theorem frrlem16

Description: Lemma for general well-founded recursion. Establish a subset relationship. (Contributed by Scott Fenton, 11-Sep-2023)

Ref Expression
Assertion frrlem16 
|- ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> A. w e. TrPred ( R , A , z ) Pred ( R , A , w ) C_ TrPred ( R , A , z ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( ( R Fr A /\ R Se A ) /\ z e. A ) /\ w e. TrPred ( R , A , z ) ) -> z e. A )
2 simpllr 
 |-  ( ( ( ( R Fr A /\ R Se A ) /\ z e. A ) /\ w e. TrPred ( R , A , z ) ) -> R Se A )
3 1 2 jca 
 |-  ( ( ( ( R Fr A /\ R Se A ) /\ z e. A ) /\ w e. TrPred ( R , A , z ) ) -> ( z e. A /\ R Se A ) )
4 simpr 
 |-  ( ( ( ( R Fr A /\ R Se A ) /\ z e. A ) /\ w e. TrPred ( R , A , z ) ) -> w e. TrPred ( R , A , z ) )
5 trpredtr 
 |-  ( ( z e. A /\ R Se A ) -> ( w e. TrPred ( R , A , z ) -> Pred ( R , A , w ) C_ TrPred ( R , A , z ) ) )
6 3 4 5 sylc 
 |-  ( ( ( ( R Fr A /\ R Se A ) /\ z e. A ) /\ w e. TrPred ( R , A , z ) ) -> Pred ( R , A , w ) C_ TrPred ( R , A , z ) )
7 6 ralrimiva 
 |-  ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> A. w e. TrPred ( R , A , z ) Pred ( R , A , w ) C_ TrPred ( R , A , z ) )