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 = ∅