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