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)

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 setlikespec 
 |-  ( ( b e. B /\ R Se B ) -> Pred ( R , B , b ) e. _V )
11 trpredpred 
 |-  ( Pred ( R , B , b ) e. _V -> Pred ( R , B , b ) C_ TrPred ( R , B , b ) )
12 ssn0 
 |-  ( ( Pred ( R , B , b ) C_ TrPred ( R , B , b ) /\ Pred ( R , B , b ) =/= (/) ) -> TrPred ( R , B , b ) =/= (/) )
13 12 ex 
 |-  ( Pred ( R , B , b ) C_ TrPred ( R , B , b ) -> ( Pred ( R , B , b ) =/= (/) -> TrPred ( R , B , b ) =/= (/) ) )
14 11 13 syl 
 |-  ( Pred ( R , B , b ) e. _V -> ( Pred ( R , B , b ) =/= (/) -> TrPred ( R , B , b ) =/= (/) ) )
15 trpredss 
 |-  ( Pred ( R , B , b ) e. _V -> TrPred ( R , B , b ) C_ B )
16 14 15 jctild 
 |-  ( Pred ( R , B , b ) e. _V -> ( Pred ( R , B , b ) =/= (/) -> ( TrPred ( R , B , b ) C_ B /\ TrPred ( R , B , b ) =/= (/) ) ) )
17 10 16 syl 
 |-  ( ( b e. B /\ R Se B ) -> ( Pred ( R , B , b ) =/= (/) -> ( TrPred ( R , B , b ) C_ B /\ TrPred ( R , B , b ) =/= (/) ) ) )
18 17 adantr 
 |-  ( ( ( b e. B /\ R Se B ) /\ R Fr B ) -> ( Pred ( R , B , b ) =/= (/) -> ( TrPred ( R , B , b ) C_ B /\ TrPred ( R , B , b ) =/= (/) ) ) )
19 trpredex 
 |-  TrPred ( R , B , b ) e. _V
20 sseq1 
 |-  ( c = TrPred ( R , B , b ) -> ( c C_ B <-> TrPred ( R , B , b ) C_ B ) )
21 neeq1 
 |-  ( c = TrPred ( R , B , b ) -> ( c =/= (/) <-> TrPred ( R , B , b ) =/= (/) ) )
22 20 21 anbi12d 
 |-  ( c = TrPred ( R , B , b ) -> ( ( c C_ B /\ c =/= (/) ) <-> ( TrPred ( R , B , b ) C_ B /\ TrPred ( R , B , b ) =/= (/) ) ) )
23 predeq2 
 |-  ( c = TrPred ( R , B , b ) -> Pred ( R , c , y ) = Pred ( R , TrPred ( R , B , b ) , y ) )
24 23 eqeq1d 
 |-  ( c = TrPred ( R , B , b ) -> ( Pred ( R , c , y ) = (/) <-> Pred ( R , TrPred ( R , B , b ) , y ) = (/) ) )
25 24 rexeqbi1dv 
 |-  ( c = TrPred ( R , B , b ) -> ( E. y e. c Pred ( R , c , y ) = (/) <-> E. y e. TrPred ( R , B , b ) Pred ( R , TrPred ( R , B , b ) , y ) = (/) ) )
26 22 25 imbi12d 
 |-  ( c = TrPred ( R , B , b ) -> ( ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) <-> ( ( TrPred ( R , B , b ) C_ B /\ TrPred ( R , B , b ) =/= (/) ) -> E. y e. TrPred ( R , B , b ) Pred ( R , TrPred ( R , B , b ) , y ) = (/) ) ) )
27 26 imbi2d 
 |-  ( c = TrPred ( R , B , b ) -> ( ( R Fr B -> ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) ) <-> ( R Fr B -> ( ( TrPred ( R , B , b ) C_ B /\ TrPred ( R , B , b ) =/= (/) ) -> E. y e. TrPred ( R , B , b ) Pred ( R , TrPred ( R , B , b ) , y ) = (/) ) ) ) )
28 dffr4 
 |-  ( R Fr B <-> A. c ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) )
29 sp 
 |-  ( A. c ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) -> ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) )
30 28 29 sylbi 
 |-  ( R Fr B -> ( ( c C_ B /\ c =/= (/) ) -> E. y e. c Pred ( R , c , y ) = (/) ) )
31 19 27 30 vtocl 
 |-  ( R Fr B -> ( ( TrPred ( R , B , b ) C_ B /\ TrPred ( R , B , b ) =/= (/) ) -> E. y e. TrPred ( R , B , b ) Pred ( R , TrPred ( R , B , b ) , y ) = (/) ) )
32 10 15 syl 
 |-  ( ( b e. B /\ R Se B ) -> TrPred ( R , B , b ) C_ B )
33 32 adantr 
 |-  ( ( ( b e. B /\ R Se B ) /\ y e. TrPred ( R , B , b ) ) -> TrPred ( R , B , b ) C_ B )
34 trpredtr 
 |-  ( ( b e. B /\ R Se B ) -> ( y e. TrPred ( R , B , b ) -> Pred ( R , B , y ) C_ TrPred ( R , B , b ) ) )
35 34 imp 
 |-  ( ( ( b e. B /\ R Se B ) /\ y e. TrPred ( R , B , b ) ) -> Pred ( R , B , y ) C_ TrPred ( R , B , b ) )
36 sspred 
 |-  ( ( TrPred ( R , B , b ) C_ B /\ Pred ( R , B , y ) C_ TrPred ( R , B , b ) ) -> Pred ( R , B , y ) = Pred ( R , TrPred ( R , B , b ) , y ) )
37 33 35 36 syl2anc 
 |-  ( ( ( b e. B /\ R Se B ) /\ y e. TrPred ( R , B , b ) ) -> Pred ( R , B , y ) = Pred ( R , TrPred ( R , B , b ) , y ) )
38 37 eqeq1d 
 |-  ( ( ( b e. B /\ R Se B ) /\ y e. TrPred ( R , B , b ) ) -> ( Pred ( R , B , y ) = (/) <-> Pred ( R , TrPred ( R , B , b ) , y ) = (/) ) )
39 38 biimprd 
 |-  ( ( ( b e. B /\ R Se B ) /\ y e. TrPred ( R , B , b ) ) -> ( Pred ( R , TrPred ( R , B , b ) , y ) = (/) -> Pred ( R , B , y ) = (/) ) )
40 39 reximdva 
 |-  ( ( b e. B /\ R Se B ) -> ( E. y e. TrPred ( R , B , b ) Pred ( R , TrPred ( R , B , b ) , y ) = (/) -> E. y e. TrPred ( R , B , b ) Pred ( R , B , y ) = (/) ) )
41 ssrexv 
 |-  ( TrPred ( R , B , b ) C_ B -> ( E. y e. TrPred ( R , B , b ) Pred ( R , B , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) )
42 32 40 41 sylsyld 
 |-  ( ( b e. B /\ R Se B ) -> ( E. y e. TrPred ( R , B , b ) Pred ( R , TrPred ( R , B , b ) , y ) = (/) -> E. y e. B Pred ( R , B , y ) = (/) ) )
43 31 42 sylan9r 
 |-  ( ( ( b e. B /\ R Se B ) /\ R Fr B ) -> ( ( TrPred ( R , B , b ) C_ B /\ TrPred ( R , B , b ) =/= (/) ) -> E. y e. B Pred ( R , B , y ) = (/) ) )
44 18 43 syld 
 |-  ( ( ( b e. B /\ R Se B ) /\ R Fr B ) -> ( Pred ( R , B , b ) =/= (/) -> E. y e. B Pred ( R , B , y ) = (/) ) )
45 44 an31s 
 |-  ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> ( Pred ( R , B , b ) =/= (/) -> E. y e. B Pred ( R , B , y ) = (/) ) )
46 9 45 pm2.61dne 
 |-  ( ( ( R Fr B /\ R Se B ) /\ b e. B ) -> E. y e. B Pred ( R , B , y ) = (/) )
47 46 ex 
 |-  ( ( R Fr B /\ R Se B ) -> ( b e. B -> E. y e. B Pred ( R , B , y ) = (/) ) )
48 47 exlimdv 
 |-  ( ( R Fr B /\ R Se B ) -> ( E. b b e. B -> E. y e. B Pred ( R , B , y ) = (/) ) )
49 4 48 syl5bi 
 |-  ( ( R Fr B /\ R Se B ) -> ( B =/= (/) -> E. y e. B Pred ( R , B , y ) = (/) ) )
50 3 49 syl6com 
 |-  ( ( R Fr A /\ R Se A ) -> ( B C_ A -> ( B =/= (/) -> E. y e. B Pred ( R , B , y ) = (/) ) ) )
51 50 imp32 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) )