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 Could not format assertion : No typesetting found for |- ( ( ( 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 ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 predres ⊢PredRAw=PredR↾AAw
2 relres ⊢Rel⁡R↾A
3 ssttrcl Could not format ( Rel ( R |` A ) -> ( R |` A ) C_ t++ ( R |` A ) ) : No typesetting found for |- ( Rel ( R |` A ) -> ( R |` A ) C_ t++ ( R |` A ) ) with typecode |-
4 2 3 ax-mp Could not format ( R |` A ) C_ t++ ( R |` A ) : No typesetting found for |- ( R |` A ) C_ t++ ( R |` A ) with typecode |-
5 predrelss Could not format ( ( R |` A ) C_ t++ ( R |` A ) -> Pred ( ( R |` A ) , A , w ) C_ Pred ( t++ ( R |` A ) , A , w ) ) : No typesetting found for |- ( ( R |` A ) C_ t++ ( R |` A ) -> Pred ( ( R |` A ) , A , w ) C_ Pred ( t++ ( R |` A ) , A , w ) ) with typecode |-
6 4 5 ax-mp Could not format Pred ( ( R |` A ) , A , w ) C_ Pred ( t++ ( R |` A ) , A , w ) : No typesetting found for |- Pred ( ( R |` A ) , A , w ) C_ Pred ( t++ ( R |` A ) , A , w ) with typecode |-
7 1 6 eqsstri Could not format Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , w ) : No typesetting found for |- Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , w ) with typecode |-
8 inss1 Could not format ( t++ ( R |` A ) i^i ( A X. A ) ) C_ t++ ( R |` A ) : No typesetting found for |- ( t++ ( R |` A ) i^i ( A X. A ) ) C_ t++ ( R |` A ) with typecode |-
9 coss1 Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
10 8 9 ax-mp Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
11 coss2 Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
12 8 11 ax-mp Could not format ( t++ ( R |` A ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) C_ ( t++ ( R |` A ) o. t++ ( R |` A ) ) : No typesetting found for |- ( t++ ( R |` A ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) C_ ( t++ ( R |` A ) o. t++ ( R |` A ) ) with typecode |-
13 10 12 sstri Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
14 ttrcltr Could not format ( t++ ( R |` A ) o. t++ ( R |` A ) ) C_ t++ ( R |` A ) : No typesetting found for |- ( t++ ( R |` A ) o. t++ ( R |` A ) ) C_ t++ ( R |` A ) with typecode |-
15 13 14 sstri Could not format ( ( t++ ( R |` A ) i^i ( A X. A ) ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) C_ t++ ( R |` A ) : No typesetting found for |- ( ( t++ ( R |` A ) i^i ( A X. A ) ) o. ( t++ ( R |` A ) i^i ( A X. A ) ) ) C_ t++ ( R |` A ) with typecode |-
16 predtrss Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
17 15 16 mp3an1 Could not format ( ( w e. Pred ( t++ ( R |` A ) , A , z ) /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) ) : No typesetting found for |- ( ( w e. Pred ( t++ ( R |` A ) , A , z ) /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) ) with typecode |-
18 7 17 sstrid Could not format ( ( w e. Pred ( t++ ( R |` A ) , A , z ) /\ z e. A ) -> Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) ) : No typesetting found for |- ( ( w e. Pred ( t++ ( R |` A ) , A , z ) /\ z e. A ) -> Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) ) with typecode |-
19 18 ancoms Could not format ( ( z e. A /\ w e. Pred ( t++ ( R |` A ) , A , z ) ) -> Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) ) : No typesetting found for |- ( ( z e. A /\ w e. Pred ( t++ ( R |` A ) , A , z ) ) -> Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) ) with typecode |-
20 19 ralrimiva Could not format ( z e. A -> A. w e. Pred ( t++ ( R |` A ) , A , z ) Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) ) : No typesetting found for |- ( z e. A -> A. w e. Pred ( t++ ( R |` A ) , A , z ) Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) ) with typecode |-
21 20 adantl Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-