Metamath Proof Explorer

Theorem fprlem2

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

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

Proof

Step Hyp Ref Expression
1 vex 
 |-  w e. _V
2 1 elpred 
 |-  ( z e. _V -> ( w e. Pred ( R , A , z ) <-> ( w e. A /\ w R z ) ) )
3 2 elv 
 |-  ( w e. Pred ( R , A , z ) <-> ( w e. A /\ w R z ) )
4 simprl 
 |-  ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) /\ ( x e. A /\ x R w ) ) -> x e. A )
5 simpll2 
 |-  ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) -> R Po A )
6 5 adantr 
 |-  ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) /\ ( x e. A /\ x R w ) ) -> R Po A )
7 simprl 
 |-  ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) -> w e. A )
8 7 adantr 
 |-  ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) /\ ( x e. A /\ x R w ) ) -> w e. A )
9 simpllr 
 |-  ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) /\ ( x e. A /\ x R w ) ) -> z e. A )
10 4 8 9 3jca 
 |-  ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) /\ ( x e. A /\ x R w ) ) -> ( x e. A /\ w e. A /\ z e. A ) )
11 6 10 jca 
 |-  ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) /\ ( x e. A /\ x R w ) ) -> ( R Po A /\ ( x e. A /\ w e. A /\ z e. A ) ) )
12 simprr 
 |-  ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) /\ ( x e. A /\ x R w ) ) -> x R w )
13 simplrr 
 |-  ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) /\ ( x e. A /\ x R w ) ) -> w R z )
14 12 13 jca 
 |-  ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) /\ ( x e. A /\ x R w ) ) -> ( x R w /\ w R z ) )
15 potr 
 |-  ( ( R Po A /\ ( x e. A /\ w e. A /\ z e. A ) ) -> ( ( x R w /\ w R z ) -> x R z ) )
16 11 14 15 sylc 
 |-  ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) /\ ( x e. A /\ x R w ) ) -> x R z )
17 4 16 jca 
 |-  ( ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) /\ ( x e. A /\ x R w ) ) -> ( x e. A /\ x R z ) )
18 17 ex 
 |-  ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) -> ( ( x e. A /\ x R w ) -> ( x e. A /\ x R z ) ) )
19 vex 
 |-  x e. _V
20 19 elpred 
 |-  ( w e. _V -> ( x e. Pred ( R , A , w ) <-> ( x e. A /\ x R w ) ) )
21 20 elv 
 |-  ( x e. Pred ( R , A , w ) <-> ( x e. A /\ x R w ) )
22 19 elpred 
 |-  ( z e. _V -> ( x e. Pred ( R , A , z ) <-> ( x e. A /\ x R z ) ) )
23 22 elv 
 |-  ( x e. Pred ( R , A , z ) <-> ( x e. A /\ x R z ) )
24 18 21 23 3imtr4g 
 |-  ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) -> ( x e. Pred ( R , A , w ) -> x e. Pred ( R , A , z ) ) )
25 24 ssrdv 
 |-  ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ ( w e. A /\ w R z ) ) -> Pred ( R , A , w ) C_ Pred ( R , A , z ) )
26 3 25 sylan2b 
 |-  ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) /\ w e. Pred ( R , A , z ) ) -> Pred ( R , A , w ) C_ Pred ( R , A , z ) )
27 26 ralrimiva 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) -> A. w e. Pred ( R , A , z ) Pred ( R , A , w ) C_ Pred ( R , A , z ) )