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 A w Pred R A z Pred R A w Pred R A z

Proof

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