Metamath Proof Explorer


Theorem frpomin

Description: Every nonempty (possibly proper) subclass of a class A with a well-founded set-like partial order R has a minimal element. The additional condition of partial order over frmin enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022)

Ref Expression
Assertion frpomin R Fr A R Po A R Se A B A B x B y B ¬ y R x

Proof

Step Hyp Ref Expression
1 n0 B z z B
2 rabeq0 w B | w R z = w B ¬ w R z
3 simprr R Fr A R Po A R Se A B A z B z B
4 breq1 y = w y R x w R x
5 4 notbid y = w ¬ y R x ¬ w R x
6 5 cbvralvw y B ¬ y R x w B ¬ w R x
7 breq2 x = z w R x w R z
8 7 notbid x = z ¬ w R x ¬ w R z
9 8 ralbidv x = z w B ¬ w R x w B ¬ w R z
10 6 9 syl5bb x = z y B ¬ y R x w B ¬ w R z
11 10 rspcev z B w B ¬ w R z x B y B ¬ y R x
12 11 ex z B w B ¬ w R z x B y B ¬ y R x
13 3 12 syl R Fr A R Po A R Se A B A z B w B ¬ w R z x B y B ¬ y R x
14 2 13 syl5bi R Fr A R Po A R Se A B A z B w B | w R z = x B y B ¬ y R x
15 simprl R Fr A R Po A R Se A B A z B B A
16 simpl3 R Fr A R Po A R Se A B A z B R Se A
17 sess2 B A R Se A R Se B
18 15 16 17 sylc R Fr A R Po A R Se A B A z B R Se B
19 seex R Se B z B w B | w R z V
20 18 3 19 syl2anc R Fr A R Po A R Se A B A z B w B | w R z V
21 simpl1 R Fr A R Po A R Se A B A z B R Fr A
22 ssrab2 w B | w R z B
23 22 15 sstrid R Fr A R Po A R Se A B A z B w B | w R z A
24 fri w B | w R z V R Fr A w B | w R z A w B | w R z x w B | w R z y w B | w R z ¬ y R x
25 24 expr w B | w R z V R Fr A w B | w R z A w B | w R z x w B | w R z y w B | w R z ¬ y R x
26 20 21 23 25 syl21anc R Fr A R Po A R Se A B A z B w B | w R z x w B | w R z y w B | w R z ¬ y R x
27 breq1 w = x w R z x R z
28 27 rexrab x w B | w R z y w B | w R z ¬ y R x x B x R z y w B | w R z ¬ y R x
29 breq1 w = y w R z y R z
30 29 ralrab y w B | w R z ¬ y R x y B y R z ¬ y R x
31 simprr R Fr A R Po A R Se A B A z B x B x R z y B y R x y R x
32 simplr R Fr A R Po A R Se A B A z B x B x R z y B y R x x R z
33 simplrl R Fr A R Po A R Se A B A z B x B B A
34 33 ad2antrr R Fr A R Po A R Se A B A z B x B x R z y B y R x B A
35 simpll2 R Fr A R Po A R Se A B A z B x B R Po A
36 35 ad2antrr R Fr A R Po A R Se A B A z B x B x R z y B y R x R Po A
37 poss B A R Po A R Po B
38 34 36 37 sylc R Fr A R Po A R Se A B A z B x B x R z y B y R x R Po B
39 simprl R Fr A R Po A R Se A B A z B x B x R z y B y R x y B
40 simpllr R Fr A R Po A R Se A B A z B x B x R z y B y R x x B
41 simplrr R Fr A R Po A R Se A B A z B x B z B
42 41 ad2antrr R Fr A R Po A R Se A B A z B x B x R z y B y R x z B
43 potr R Po B y B x B z B y R x x R z y R z
44 38 39 40 42 43 syl13anc R Fr A R Po A R Se A B A z B x B x R z y B y R x y R x x R z y R z
45 31 32 44 mp2and R Fr A R Po A R Se A B A z B x B x R z y B y R x y R z
46 45 expr R Fr A R Po A R Se A B A z B x B x R z y B y R x y R z
47 46 con3d R Fr A R Po A R Se A B A z B x B x R z y B ¬ y R z ¬ y R x
48 idd R Fr A R Po A R Se A B A z B x B x R z y B ¬ y R x ¬ y R x
49 47 48 jad R Fr A R Po A R Se A B A z B x B x R z y B y R z ¬ y R x ¬ y R x
50 49 ralimdva R Fr A R Po A R Se A B A z B x B x R z y B y R z ¬ y R x y B ¬ y R x
51 30 50 syl5bi R Fr A R Po A R Se A B A z B x B x R z y w B | w R z ¬ y R x y B ¬ y R x
52 51 expimpd R Fr A R Po A R Se A B A z B x B x R z y w B | w R z ¬ y R x y B ¬ y R x
53 52 reximdva R Fr A R Po A R Se A B A z B x B x R z y w B | w R z ¬ y R x x B y B ¬ y R x
54 28 53 syl5bi R Fr A R Po A R Se A B A z B x w B | w R z y w B | w R z ¬ y R x x B y B ¬ y R x
55 26 54 syld R Fr A R Po A R Se A B A z B w B | w R z x B y B ¬ y R x
56 14 55 pm2.61dne R Fr A R Po A R Se A B A z B x B y B ¬ y R x
57 56 expr R Fr A R Po A R Se A B A z B x B y B ¬ y R x
58 57 exlimdv R Fr A R Po A R Se A B A z z B x B y B ¬ y R x
59 1 58 syl5bi R Fr A R Po A R Se A B A B x B y B ¬ y R x
60 59 impr R Fr A R Po A R Se A B A B x B y B ¬ y R x