Metamath Proof Explorer


Theorem frpoind

Description: The principle of well-founded induction over a partial order. This theorem is a version of frind that does not require the axiom of infinity and can be used to prove wfi and tfi . (Contributed by Scott Fenton, 11-Feb-2022)

Ref Expression
Assertion frpoind R Fr A R Po A R Se A B A y A Pred R A y B y B A = B

Proof

Step Hyp Ref Expression
1 ssdif0 A B A B =
2 1 necon3bbii ¬ A B A B
3 difss A B A
4 frpomin2 R Fr A R Po A R Se A A B A A B y A B Pred R A B y =
5 eldif y A B y A ¬ y B
6 5 anbi1i y A B Pred R A B y = y A ¬ y B Pred R A B y =
7 anass y A ¬ y B Pred R A B y = y A ¬ y B Pred R A B y =
8 indif2 R -1 y A B = R -1 y A B
9 df-pred Pred R A B y = A B R -1 y
10 incom A B R -1 y = R -1 y A B
11 9 10 eqtri Pred R A B y = R -1 y A B
12 df-pred Pred R A y = A R -1 y
13 incom A R -1 y = R -1 y A
14 12 13 eqtri Pred R A y = R -1 y A
15 14 difeq1i Pred R A y B = R -1 y A B
16 8 11 15 3eqtr4i Pred R A B y = Pred R A y B
17 16 eqeq1i Pred R A B y = Pred R A y B =
18 ssdif0 Pred R A y B Pred R A y B =
19 17 18 bitr4i Pred R A B y = Pred R A y B
20 19 anbi1ci ¬ y B Pred R A B y = Pred R A y B ¬ y B
21 20 anbi2i y A ¬ y B Pred R A B y = y A Pred R A y B ¬ y B
22 6 7 21 3bitri y A B Pred R A B y = y A Pred R A y B ¬ y B
23 22 rexbii2 y A B Pred R A B y = y A Pred R A y B ¬ y B
24 rexanali y A Pred R A y B ¬ y B ¬ y A Pred R A y B y B
25 23 24 bitri y A B Pred R A B y = ¬ y A Pred R A y B y B
26 4 25 sylib R Fr A R Po A R Se A A B A A B ¬ y A Pred R A y B y B
27 26 ex R Fr A R Po A R Se A A B A A B ¬ y A Pred R A y B y B
28 3 27 mpani R Fr A R Po A R Se A A B ¬ y A Pred R A y B y B
29 2 28 syl5bi R Fr A R Po A R Se A ¬ A B ¬ y A Pred R A y B y B
30 29 con4d R Fr A R Po A R Se A y A Pred R A y B y B A B
31 30 imp R Fr A R Po A R Se A y A Pred R A y B y B A B
32 31 adantrl R Fr A R Po A R Se A B A y A Pred R A y B y B A B
33 simprl R Fr A R Po A R Se A B A y A Pred R A y B y B B A
34 32 33 eqssd R Fr A R Po A R Se A B A y A Pred R A y B y B A = B