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 ⊢RFrA∧RSeA∧B⊆A∧B≠∅→∃y∈BPredRBy=∅

Proof

Step Hyp Ref Expression
1 frss ⊢B⊆A→RFrA→RFrB
2 sess2 ⊢B⊆A→RSeA→RSeB
3 1 2 anim12d ⊢B⊆A→RFrA∧RSeA→RFrB∧RSeB
4 n0 ⊢B≠∅↔∃bb∈B
5 predeq3 ⊢y=b→PredRBy=PredRBb
6 5 eqeq1d ⊢y=b→PredRBy=∅↔PredRBb=∅
7 6 rspcev ⊢b∈B∧PredRBb=∅→∃y∈BPredRBy=∅
8 7 ex ⊢b∈B→PredRBb=∅→∃y∈BPredRBy=∅
9 8 adantl ⊢RFrB∧RSeB∧b∈B→PredRBb=∅→∃y∈BPredRBy=∅
10 predres ⊢PredRBb=PredR↾BBb
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→PredR↾BBb⊆Predt++R↾BBb
15 13 14 ax-mp ⊢PredR↾BBb⊆Predt++R↾BBb
16 10 15 eqsstri ⊢PredRBb⊆Predt++R↾BBb
17 ssn0 ⊢PredRBb⊆Predt++R↾BBb∧PredRBb≠∅→Predt++R↾BBb≠∅
18 16 17 mpan ⊢PredRBb≠∅→Predt++R↾BBb≠∅
19 predss ⊢Predt++R↾BBb⊆B
20 18 19 jctil ⊢PredRBb≠∅→Predt++R↾BBb⊆B∧Predt++R↾BBb≠∅
21 dffr4 ⊢RFrB↔∀cc⊆B∧c≠∅→∃y∈cPredRcy=∅
22 21 biimpi ⊢RFrB→∀cc⊆B∧c≠∅→∃y∈cPredRcy=∅
23 ttrclse ⊢RSeB→t++R↾BSeB
24 setlikespec ⊢b∈B∧t++R↾BSeB→Predt++R↾BBb∈V
25 23 24 sylan2 ⊢b∈B∧RSeB→Predt++R↾BBb∈V
26 25 ancoms ⊢RSeB∧b∈B→Predt++R↾BBb∈V
27 sseq1 ⊢c=Predt++R↾BBb→c⊆B↔Predt++R↾BBb⊆B
28 neeq1 ⊢c=Predt++R↾BBb→c≠∅↔Predt++R↾BBb≠∅
29 27 28 anbi12d ⊢c=Predt++R↾BBb→c⊆B∧c≠∅↔Predt++R↾BBb⊆B∧Predt++R↾BBb≠∅
30 predeq2 ⊢c=Predt++R↾BBb→PredRcy=PredRPredt++R↾BBby
31 30 eqeq1d ⊢c=Predt++R↾BBb→PredRcy=∅↔PredRPredt++R↾BBby=∅
32 31 rexeqbi1dv ⊢c=Predt++R↾BBb→∃y∈cPredRcy=∅↔∃y∈Predt++R↾BBbPredRPredt++R↾BBby=∅
33 29 32 imbi12d ⊢c=Predt++R↾BBb→c⊆B∧c≠∅→∃y∈cPredRcy=∅↔Predt++R↾BBb⊆B∧Predt++R↾BBb≠∅→∃y∈Predt++R↾BBbPredRPredt++R↾BBby=∅
34 33 spcgv ⊢Predt++R↾BBb∈V→∀cc⊆B∧c≠∅→∃y∈cPredRcy=∅→Predt++R↾BBb⊆B∧Predt++R↾BBb≠∅→∃y∈Predt++R↾BBbPredRPredt++R↾BBby=∅
35 34 impcom ⊢∀cc⊆B∧c≠∅→∃y∈cPredRcy=∅∧Predt++R↾BBb∈V→Predt++R↾BBb⊆B∧Predt++R↾BBb≠∅→∃y∈Predt++R↾BBbPredRPredt++R↾BBby=∅
36 22 26 35 syl2an ⊢RFrB∧RSeB∧b∈B→Predt++R↾BBb⊆B∧Predt++R↾BBb≠∅→∃y∈Predt++R↾BBbPredRPredt++R↾BBby=∅
37 36 anassrs ⊢RFrB∧RSeB∧b∈B→Predt++R↾BBb⊆B∧Predt++R↾BBb≠∅→∃y∈Predt++R↾BBbPredRPredt++R↾BBby=∅
38 predres ⊢PredRBy=PredR↾BBy
39 predrelss ⊢R↾B⊆t++R↾B→PredR↾BBy⊆Predt++R↾BBy
40 13 39 ax-mp ⊢PredR↾BBy⊆Predt++R↾BBy
41 38 40 eqsstri ⊢PredRBy⊆Predt++R↾BBy
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∈Predt++R↾BBb∧b∈B→Predt++R↾BBy⊆Predt++R↾BBb
51 49 50 mp3an1 ⊢y∈Predt++R↾BBb∧b∈B→Predt++R↾BBy⊆Predt++R↾BBb
52 41 51 sstrid ⊢y∈Predt++R↾BBb∧b∈B→PredRBy⊆Predt++R↾BBb
53 sspred ⊢Predt++R↾BBb⊆B∧PredRBy⊆Predt++R↾BBb→PredRBy=PredRPredt++R↾BBby
54 19 52 53 sylancr ⊢y∈Predt++R↾BBb∧b∈B→PredRBy=PredRPredt++R↾BBby
55 54 ancoms ⊢b∈B∧y∈Predt++R↾BBb→PredRBy=PredRPredt++R↾BBby
56 55 eqeq1d ⊢b∈B∧y∈Predt++R↾BBb→PredRBy=∅↔PredRPredt++R↾BBby=∅
57 56 rexbidva ⊢b∈B→∃y∈Predt++R↾BBbPredRBy=∅↔∃y∈Predt++R↾BBbPredRPredt++R↾BBby=∅
58 ssrexv ⊢Predt++R↾BBb⊆B→∃y∈Predt++R↾BBbPredRBy=∅→∃y∈BPredRBy=∅
59 19 58 ax-mp ⊢∃y∈Predt++R↾BBbPredRBy=∅→∃y∈BPredRBy=∅
60 57 59 biimtrrdi ⊢b∈B→∃y∈Predt++R↾BBbPredRPredt++R↾BBby=∅→∃y∈BPredRBy=∅
61 60 adantl ⊢RFrB∧RSeB∧b∈B→∃y∈Predt++R↾BBbPredRPredt++R↾BBby=∅→∃y∈BPredRBy=∅
62 37 61 syld ⊢RFrB∧RSeB∧b∈B→Predt++R↾BBb⊆B∧Predt++R↾BBb≠∅→∃y∈BPredRBy=∅
63 20 62 syl5 ⊢RFrB∧RSeB∧b∈B→PredRBb≠∅→∃y∈BPredRBy=∅
64 9 63 pm2.61dne ⊢RFrB∧RSeB∧b∈B→∃y∈BPredRBy=∅
65 64 ex ⊢RFrB∧RSeB→b∈B→∃y∈BPredRBy=∅
66 65 exlimdv ⊢RFrB∧RSeB→∃bb∈B→∃y∈BPredRBy=∅
67 4 66 biimtrid ⊢RFrB∧RSeB→B≠∅→∃y∈BPredRBy=∅
68 3 67 syl6com ⊢RFrA∧RSeA→B⊆A→B≠∅→∃y∈BPredRBy=∅
69 68 imp32 ⊢RFrA∧RSeA∧B⊆A∧B≠∅→∃y∈BPredRBy=∅