Metamath Proof Explorer


Theorem frmin

Description: Every (possibly proper) subclass of a class A with a well-founded set-like relation R has a minimal element. This is a very strong generalization of tz6.26 and tz7.5 . (Contributed by Scott Fenton, 4-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by Scott Fenton, 27-Nov-2024)

Ref Expression
Assertion frmin R Fr A R Se A B A B y B Pred R B y =

Proof

Step Hyp Ref Expression
1 frss B A R Fr A R Fr B
2 sess2 B A R Se A R Se B
3 1 2 anim12d B A R Fr A R Se A R Fr B R Se B
4 n0 B b b B
5 predeq3 y = b Pred R B y = Pred R B b
6 5 eqeq1d y = b Pred R B y = Pred R B b =
7 6 rspcev b B Pred R B b = y B Pred R B y =
8 7 ex b B Pred R B b = y B Pred R B y =
9 8 adantl R Fr B R Se B b B Pred R B b = y B Pred R B y =
10 predres Pred R B b = Pred R B B b
11 relres Rel R B
12 ssttrcl Rel R B R B t++ R B
13 11 12 ax-mp R B t++ R B
14 predrelss R B t++ R B Pred R B B b Pred t++ R B B b
15 13 14 ax-mp Pred R B B b Pred t++ R B B b
16 10 15 eqsstri Pred R B b Pred t++ R B B b
17 ssn0 Pred R B b Pred t++ R B B b Pred R B b Pred t++ R B B b
18 16 17 mpan Pred R B b Pred t++ R B B b
19 predss Pred t++ R B B b B
20 18 19 jctil Pred R B b Pred t++ R B B b B Pred t++ R B B b
21 dffr4 R Fr B c c B c y c Pred R c y =
22 21 biimpi R Fr B c c B c y c Pred R c y =
23 ttrclse R Se B t++ R B Se B
24 setlikespec b B t++ R B Se B Pred t++ R B B b V
25 23 24 sylan2 b B R Se B Pred t++ R B B b V
26 25 ancoms R Se B b B Pred t++ R B B b V
27 sseq1 c = Pred t++ R B B b c B Pred t++ R B B b B
28 neeq1 c = Pred t++ R B B b c Pred t++ R B B b
29 27 28 anbi12d c = Pred t++ R B B b c B c Pred t++ R B B b B Pred t++ R B B b
30 predeq2 c = Pred t++ R B B b Pred R c y = Pred R Pred t++ R B B b y
31 30 eqeq1d c = Pred t++ R B B b Pred R c y = Pred R Pred t++ R B B b y =
32 31 rexeqbi1dv c = Pred t++ R B B b y c Pred R c y = y Pred t++ R B B b Pred R Pred t++ R B B b y =
33 29 32 imbi12d c = Pred t++ R B B b c B c y c Pred R c y = Pred t++ R B B b B Pred t++ R B B b y Pred t++ R B B b Pred R Pred t++ R B B b y =
34 33 spcgv Pred t++ R B B b V c c B c y c Pred R c y = Pred t++ R B B b B Pred t++ R B B b y Pred t++ R B B b Pred R Pred t++ R B B b y =
35 34 impcom c c B c y c Pred R c y = Pred t++ R B B b V Pred t++ R B B b B Pred t++ R B B b y Pred t++ R B B b Pred R Pred t++ R B B b y =
36 22 26 35 syl2an R Fr B R Se B b B Pred t++ R B B b B Pred t++ R B B b y Pred t++ R B B b Pred R Pred t++ R B B b y =
37 36 anassrs R Fr B R Se B b B Pred t++ R B B b B Pred t++ R B B b y Pred t++ R B B b Pred R Pred t++ R B B b y =
38 predres Pred R B y = Pred R B B y
39 predrelss R B t++ R B Pred R B B y Pred t++ R B B y
40 13 39 ax-mp Pred R B B y Pred t++ R B B y
41 38 40 eqsstri Pred R B y Pred t++ R B B y
42 inss1 t++ R B B × B t++ R B
43 coss1 t++ R B B × B t++ R B t++ R B B × B t++ R B B × B t++ R B t++ R B B × B
44 42 43 ax-mp t++ R B B × B t++ R B B × B t++ R B t++ R B B × B
45 coss2 t++ R B B × B t++ R B t++ R B t++ R B B × B t++ R B t++ R B
46 42 45 ax-mp t++ R B t++ R B B × B t++ R B t++ R B
47 44 46 sstri t++ R B B × B t++ R B B × B t++ R B t++ R B
48 ttrcltr t++ R B t++ R B t++ R B
49 47 48 sstri t++ R B B × B t++ R B B × B t++ R B
50 predtrss t++ R B B × B t++ R B B × B t++ R B y Pred t++ R B B b b B Pred t++ R B B y Pred t++ R B B b
51 49 50 mp3an1 y Pred t++ R B B b b B Pred t++ R B B y Pred t++ R B B b
52 41 51 sstrid y Pred t++ R B B b b B Pred R B y Pred t++ R B B b
53 sspred Pred t++ R B B b B Pred R B y Pred t++ R B B b Pred R B y = Pred R Pred t++ R B B b y
54 19 52 53 sylancr y Pred t++ R B B b b B Pred R B y = Pred R Pred t++ R B B b y
55 54 ancoms b B y Pred t++ R B B b Pred R B y = Pred R Pred t++ R B B b y
56 55 eqeq1d b B y Pred t++ R B B b Pred R B y = Pred R Pred t++ R B B b y =
57 56 rexbidva b B y Pred t++ R B B b Pred R B y = y Pred t++ R B B b Pred R Pred t++ R B B b y =
58 ssrexv Pred t++ R B B b B y Pred t++ R B B b Pred R B y = y B Pred R B y =
59 19 58 ax-mp y Pred t++ R B B b Pred R B y = y B Pred R B y =
60 57 59 biimtrrdi b B y Pred t++ R B B b Pred R Pred t++ R B B b y = y B Pred R B y =
61 60 adantl R Fr B R Se B b B y Pred t++ R B B b Pred R Pred t++ R B B b y = y B Pred R B y =
62 37 61 syld R Fr B R Se B b B Pred t++ R B B b B Pred t++ R B B b y B Pred R B y =
63 20 62 syl5 R Fr B R Se B b B Pred R B b y B Pred R B y =
64 9 63 pm2.61dne R Fr B R Se B b B y B Pred R B y =
65 64 ex R Fr B R Se B b B y B Pred R B y =
66 65 exlimdv R Fr B R Se B b b B y B Pred R B y =
67 4 66 biimtrid R Fr B R Se B B y B Pred R B y =
68 3 67 syl6com R Fr A R Se A B A B y B Pred R B y =
69 68 imp32 R Fr A R Se A B A B y B Pred R B y =