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 ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ )

Proof

Step Hyp Ref Expression
1 frss ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Fr 𝐴 → 𝑅 Fr 𝐵 ) )
2 sess2 ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑅 Se 𝐴 → 𝑅 Se 𝐵 ) )
3 1 2 anim12d ⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) ) )
4 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ 𝐵 )
5 predeq3 ⊢ ( 𝑦 = 𝑏 → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , 𝐵 , 𝑏 ) )
6 5 eqeq1d ⊢ ( 𝑦 = 𝑏 → ( Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ↔ Pred ( 𝑅 , 𝐵 , 𝑏 ) = ∅ ) )
7 6 rspcev ⊢ ( ( 𝑏 ∈ 𝐵 ∧ Pred ( 𝑅 , 𝐵 , 𝑏 ) = ∅ ) → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ )
8 7 ex ⊢ ( 𝑏 ∈ 𝐵 → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) = ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
9 8 adantl ⊢ ( ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) = ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
10 setlikespec ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) → Pred ( 𝑅 , 𝐵 , 𝑏 ) ∈ V )
11 trpredpred ⊢ ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ∈ V → Pred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ TrPred ( 𝑅 , 𝐵 , 𝑏 ) )
12 ssn0 ⊢ ( ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ∧ Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) → TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ )
13 12 ex ⊢ ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ TrPred ( 𝑅 , 𝐵 , 𝑏 ) → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ → TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) )
14 11 13 syl ⊢ ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ∈ V → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ → TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) )
15 trpredss ⊢ ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ∈ V → TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 )
16 14 15 jctild ⊢ ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ∈ V → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ → ( TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) ) )
17 10 16 syl ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ → ( TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) ) )
18 17 adantr ⊢ ( ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑅 Fr 𝐵 ) → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ → ( TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) ) )
19 trpredex ⊢ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ∈ V
20 sseq1 ⊢ ( 𝑐 = TrPred ( 𝑅 , 𝐵 , 𝑏 ) → ( 𝑐 ⊆ 𝐵 ↔ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 ) )
21 neeq1 ⊢ ( 𝑐 = TrPred ( 𝑅 , 𝐵 , 𝑏 ) → ( 𝑐 ≠ ∅ ↔ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) )
22 20 21 anbi12d ⊢ ( 𝑐 = TrPred ( 𝑅 , 𝐵 , 𝑏 ) → ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) ↔ ( TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) ) )
23 predeq2 ⊢ ( 𝑐 = TrPred ( 𝑅 , 𝐵 , 𝑏 ) → Pred ( 𝑅 , 𝑐 , 𝑦 ) = Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) )
24 23 eqeq1d ⊢ ( 𝑐 = TrPred ( 𝑅 , 𝐵 , 𝑏 ) → ( Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ↔ Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) )
25 24 rexeqbi1dv ⊢ ( 𝑐 = TrPred ( 𝑅 , 𝐵 , 𝑏 ) → ( ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) )
26 22 25 imbi12d ⊢ ( 𝑐 = TrPred ( 𝑅 , 𝐵 , 𝑏 ) → ( ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ) ↔ ( ( TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) → ∃ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) ) )
27 26 imbi2d ⊢ ( 𝑐 = TrPred ( 𝑅 , 𝐵 , 𝑏 ) → ( ( 𝑅 Fr 𝐵 → ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ) ) ↔ ( 𝑅 Fr 𝐵 → ( ( TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) → ∃ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) ) ) )
28 dffr4 ⊢ ( 𝑅 Fr 𝐵 ↔ ∀ 𝑐 ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ) )
29 sp ⊢ ( ∀ 𝑐 ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ) → ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ) )
30 28 29 sylbi ⊢ ( 𝑅 Fr 𝐵 → ( ( 𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑐 Pred ( 𝑅 , 𝑐 , 𝑦 ) = ∅ ) )
31 19 27 30 vtocl ⊢ ( 𝑅 Fr 𝐵 → ( ( TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) → ∃ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) )
32 10 15 syl ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) → TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 )
33 32 adantr ⊢ ( ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ) → TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 )
34 trpredtr ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) → ( 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) → Pred ( 𝑅 , 𝐵 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ) )
35 34 imp ⊢ ( ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ) → Pred ( 𝑅 , 𝐵 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐵 , 𝑏 ) )
36 sspred ⊢ ( ( TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐵 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ) → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) )
37 33 35 36 syl2anc ⊢ ( ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ) → Pred ( 𝑅 , 𝐵 , 𝑦 ) = Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) )
38 37 eqeq1d ⊢ ( ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ) → ( Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ↔ Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ ) )
39 38 biimprd ⊢ ( ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ) → ( Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ → Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
40 39 reximdva ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) → ( ∃ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ → ∃ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
41 ssrexv ⊢ ( TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 → ( ∃ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
42 32 40 41 sylsyld ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) → ( ∃ 𝑦 ∈ TrPred ( 𝑅 , 𝐵 , 𝑏 ) Pred ( 𝑅 , TrPred ( 𝑅 , 𝐵 , 𝑏 ) , 𝑦 ) = ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
43 31 42 sylan9r ⊢ ( ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑅 Fr 𝐵 ) → ( ( TrPred ( 𝑅 , 𝐵 , 𝑏 ) ⊆ 𝐵 ∧ TrPred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
44 18 43 syld ⊢ ( ( ( 𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑅 Fr 𝐵 ) → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
45 44 an31s ⊢ ( ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( Pred ( 𝑅 , 𝐵 , 𝑏 ) ≠ ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
46 9 45 pm2.61dne ⊢ ( ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ )
47 46 ex ⊢ ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) → ( 𝑏 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
48 47 exlimdv ⊢ ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) → ( ∃ 𝑏 𝑏 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
49 4 48 syl5bi ⊢ ( ( 𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵 ) → ( 𝐵 ≠ ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) )
50 3 49 syl6com ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐵 ⊆ 𝐴 → ( 𝐵 ≠ ∅ → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ ) ) )
51 50 imp32 ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑦 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑦 ) = ∅ )