Metamath Proof Explorer

Theorem frrlem16

Description: Lemma for general well-founded recursion. Establish a subset relation. (Contributed by Scott Fenton, 11-Sep-2023) Revised notion of transitive closure. (Revised by Scott Fenton, 1-Dec-2024)

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

Proof

Step Hyp Ref Expression
1 predres 
 |-  Pred ( R , A , w ) = Pred ( ( R |` A ) , A , w )
2 relres 
 |-  Rel ( R |` A )
3 ssttrcl 
 |-  ( Rel ( R |` A ) -> ( R |` A ) C_ t++ ( R |` A ) )
4 2 3 ax-mp 
 |-  ( R |` A ) C_ t++ ( R |` A )
5 predrelss 
 |-  ( ( R |` A ) C_ t++ ( R |` A ) -> Pred ( ( R |` A ) , A , w ) C_ Pred ( t++ ( R |` A ) , A , w ) )
6 4 5 ax-mp 
 |-  Pred ( ( R |` A ) , A , w ) C_ Pred ( t++ ( R |` A ) , A , w )
7 1 6 eqsstri 
 |-  Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , w )
8 inss1 
 |-  ( t++ ( R |` A ) i^i ( A X. A ) ) C_ t++ ( R |` A )
9 coss1 
 |-  ( ( t++ ( R |` A ) i^i ( A X. A ) ) C_ t++ ( R |` A ) -> ( ( t++ ( R |` A ) i^i ( A X. A ) ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) C_ ( t++ ( R |` A ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) )
10 8 9 ax-mp 
 |-  ( ( t++ ( R |` A ) i^i ( A X. A ) ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) C_ ( t++ ( R |` A ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) )
11 coss2 
 |-  ( ( t++ ( R |` A ) i^i ( A X. A ) ) C_ t++ ( R |` A ) -> ( t++ ( R |` A ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) C_ ( t++ ( R |` A ) o. t++ ( R |` A ) ) )
12 8 11 ax-mp 
 |-  ( t++ ( R |` A ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) C_ ( t++ ( R |` A ) o. t++ ( R |` A ) )
13 10 12 sstri 
 |-  ( ( t++ ( R |` A ) i^i ( A X. A ) ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) C_ ( t++ ( R |` A ) o. t++ ( R |` A ) )
14 ttrcltr 
 |-  ( t++ ( R |` A ) o. t++ ( R |` A ) ) C_ t++ ( R |` A )
15 13 14 sstri 
 |-  ( ( t++ ( R |` A ) i^i ( A X. A ) ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) C_ t++ ( R |` A )
16 predtrss 
 |-  ( ( ( ( t++ ( R |` A ) i^i ( A X. A ) ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) C_ t++ ( R |` A ) /\ w e. Pred ( t++ ( R |` A ) , A , z ) /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) )
17 15 16 mp3an1 
 |-  ( ( w e. Pred ( t++ ( R |` A ) , A , z ) /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) )
18 7 17 sstrid 
 |-  ( ( w e. Pred ( t++ ( R |` A ) , A , z ) /\ z e. A ) -> Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) )
19 18 ancoms 
 |-  ( ( z e. A /\ w e. Pred ( t++ ( R |` A ) , A , z ) ) -> Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) )
20 19 ralrimiva 
 |-  ( z e. A -> A. w e. Pred ( t++ ( R |` A ) , A , z ) Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) )
21 20 adantl 
 |-  ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> A. w e. Pred ( t++ ( R |` A ) , A , z ) Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) )