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 C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) )

Proof

Step Hyp Ref Expression
1 frss 
 |-  ( B C_ A -> ( R Fr A -> R Fr B ) )
2 sess2 
 |-  ( B C_ A -> ( R Se A -> R Se B ) )
3 1 2 anim12d 
 |-  ( B C_ A -> ( ( R Fr A /\ R Se A ) -> ( R Fr B /\ R Se B ) ) )
4 n0 
 |-  ( B =/= (/) <-> E. b b e. 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 e. B /\ Pred ( R , B , b ) = (/) ) -> E. y e. B Pred ( R , B , y ) = (/) )
8 7 ex 
 |-  ( b e. B -> ( Pred ( R , B , b ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) )
9 8 adantl 
 |-  ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> ( Pred ( R , B , b ) = (/) -> E. y e. 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 ) C_ t++ ( R |` B ) )
13 11 12 ax-mp 
 |-  ( R |` B ) C_ t++ ( R |` B )
14 predrelss 
 |-  ( ( R |` B ) C_ t++ ( R |` B ) -> Pred ( ( R |` B ) , B , b ) C_ Pred ( t++ ( R |` B ) , B , b ) )
15 13 14 ax-mp 
 |-  Pred ( ( R |` B ) , B , b ) C_ Pred ( t++ ( R |` B ) , B , b )
16 10 15 eqsstri 
 |-  Pred ( R , B , b ) C_ Pred ( t++ ( R |` B ) , B , b )
17 ssn0 
 |-  ( ( Pred ( R , B , b ) C_ 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 ) C_ B
20 18 19 jctil 
 |-  ( Pred ( R , B , b ) =/= (/) -> ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) )
21 dffr4 
 |-  ( R Fr B <-> A. c ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) )
22 21 biimpi 
 |-  ( R Fr B -> A. c ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) )
23 ttrclse 
 |-  ( R Se B -> t++ ( R |` B ) Se B )
24 setlikespec 
 |-  ( ( b e. B /\ t++ ( R |` B ) Se B ) -> Pred ( t++ ( R |` B ) , B , b ) e. _V )
25 23 24 sylan2 
 |-  ( ( b e. B /\ R Se B ) -> Pred ( t++ ( R |` B ) , B , b ) e. _V )
26 25 ancoms 
 |-  ( ( R Se B /\ b e. B ) -> Pred ( t++ ( R |` B ) , B , b ) e. _V )
27 sseq1 
 |-  ( c = Pred ( t++ ( R |` B ) , B , b ) -> ( c C_ B <-> Pred ( t++ ( R |` B ) , B , b ) C_ 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 C_ B /\ c =/= (/) ) <-> ( Pred ( t++ ( R |` B ) , B , b ) C_ 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 ) -> ( E. y e. c Pred ( R , c , y ) = (/) <-> E. y e. 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 C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) <-> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) )
34 33 spcgv 
 |-  ( Pred ( t++ ( R |` B ) , B , b ) e. _V -> ( A. c ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) ) )
35 34 impcom 
 |-  ( ( A. c ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) /\ Pred ( t++ ( R |` B ) , B , b ) e. _V ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. 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 e. B ) ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. 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 e. B ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. 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 ) C_ t++ ( R |` B ) -> Pred ( ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , y ) )
40 13 39 ax-mp 
 |-  Pred ( ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , y )
41 38 40 eqsstri 
 |-  Pred ( R , B , y ) C_ Pred ( t++ ( R |` B ) , B , y )
42 inss1 
 |-  ( t++ ( R |` B ) i^i ( B X. B ) ) C_ t++ ( R |` B )
43 coss1 
 |-  ( ( t++ ( R |` B ) i^i ( B X. B ) ) C_ t++ ( R |` B ) -> ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) )
44 42 43 ax-mp 
 |-  ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) )
45 coss2 
 |-  ( ( t++ ( R |` B ) i^i ( B X. B ) ) C_ t++ ( R |` B ) -> ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. t++ ( R |` B ) ) )
46 42 45 ax-mp 
 |-  ( t++ ( R |` B ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. t++ ( R |` B ) )
47 44 46 sstri 
 |-  ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ ( t++ ( R |` B ) o. t++ ( R |` B ) )
48 ttrcltr 
 |-  ( t++ ( R |` B ) o. t++ ( R |` B ) ) C_ t++ ( R |` B )
49 47 48 sstri 
 |-  ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ t++ ( R |` B )
50 predtrss 
 |-  ( ( ( ( t++ ( R |` B ) i^i ( B X. B ) ) o. ( t++ ( R |` B ) i^i ( B X. B ) ) ) C_ t++ ( R |` B ) /\ y e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( t++ ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , b ) )
51 49 50 mp3an1 
 |-  ( ( y e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( t++ ( R |` B ) , B , y ) C_ Pred ( t++ ( R |` B ) , B , b ) )
52 41 51 sstrid 
 |-  ( ( y e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( R , B , y ) C_ Pred ( t++ ( R |` B ) , B , b ) )
53 sspred 
 |-  ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( R , B , y ) C_ 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 e. Pred ( t++ ( R |` B ) , B , b ) /\ b e. B ) -> Pred ( R , B , y ) = Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) )
55 54 ancoms 
 |-  ( ( b e. B /\ y e. Pred ( t++ ( R |` B ) , B , b ) ) -> Pred ( R , B , y ) = Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) )
56 55 eqeq1d 
 |-  ( ( b e. B /\ y e. Pred ( t++ ( R |` B ) , B , b ) ) -> ( Pred ( R , B , y ) = (/) <-> Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) )
57 56 rexbidva 
 |-  ( b e. B -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , B , y ) = (/) <-> E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) ) )
58 ssrexv 
 |-  ( Pred ( t++ ( R |` B ) , B , b ) C_ B -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , B , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) )
59 19 58 ax-mp 
 |-  ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , B , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) )
60 57 59 biimtrrdi 
 |-  ( b e. B -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) )
61 60 adantl 
 |-  ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> ( E. y e. Pred ( t++ ( R |` B ) , B , b ) Pred ( R , Pred ( t++ ( R |` B ) , B , b ) , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) )
62 37 61 syld 
 |-  ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> ( ( Pred ( t++ ( R |` B ) , B , b ) C_ B /\ Pred ( t++ ( R |` B ) , B , b ) =/= (/) ) -> E. y e. B Pred ( R , B , y ) = (/) ) )
63 20 62 syl5 
 |-  ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> ( Pred ( R , B , b ) =/= (/) -> E. y e. B Pred ( R , B , y ) = (/) ) )
64 9 63 pm2.61dne 
 |-  ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> E. y e. B Pred ( R , B , y ) = (/) )
65 64 ex 
 |-  ( ( R Fr B /\ R Se B ) -> ( b e. B -> E. y e. B Pred ( R , B , y ) = (/) ) )
66 65 exlimdv 
 |-  ( ( R Fr B /\ R Se B ) -> ( E. b b e. B -> E. y e. B Pred ( R , B , y ) = (/) ) )
67 4 66 biimtrid 
 |-  ( ( R Fr B /\ R Se B ) -> ( B =/= (/) -> E. y e. B Pred ( R , B , y ) = (/) ) )
68 3 67 syl6com 
 |-  ( ( R Fr A /\ R Se A ) -> ( B C_ A -> ( B =/= (/) -> E. y e. B Pred ( R , B , y ) = (/) ) ) )
69 68 imp32 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) )