Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frmin Structured version   Visualization version   GIF version

Theorem frmin 32057
Description: Every (possibly proper) subclass of a class 𝐴 with a founded, set-like relation 𝑅 has a minimal element. Lemma 4.3 of Don Monk's notes for Advanced Set Theory, which can be found at http://euclid.colorado.edu/~monkd/settheory. This is a very strong generalization of tz6.26 5918 and tz7.5 5951. (Contributed by Scott Fenton, 4-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
Assertion
Ref Expression
frmin (((𝑅 Fr 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
Distinct variable groups:   𝑦,𝐵   𝑦,𝑅
Allowed substitution hint:   𝐴(𝑦)

Proof of Theorem frmin
Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frss 5272 . . . 4 (𝐵𝐴 → (𝑅 Fr 𝐴𝑅 Fr 𝐵))
2 sess2 5274 . . . 4 (𝐵𝐴 → (𝑅 Se 𝐴𝑅 Se 𝐵))
31, 2anim12d 598 . . 3 (𝐵𝐴 → ((𝑅 Fr 𝐴𝑅 Se 𝐴) → (𝑅 Fr 𝐵𝑅 Se 𝐵)))
4 n0 4126 . . . 4 (𝐵 ≠ ∅ ↔ ∃𝑏 𝑏𝐵)
5 predeq3 5891 . . . . . . . . . . 11 (𝑦 = 𝑏 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐵, 𝑏))
65eqeq1d 2804 . . . . . . . . . 10 (𝑦 = 𝑏 → (Pred(𝑅, 𝐵, 𝑦) = ∅ ↔ Pred(𝑅, 𝐵, 𝑏) = ∅))
76rspcev 3498 . . . . . . . . 9 ((𝑏𝐵 ∧ Pred(𝑅, 𝐵, 𝑏) = ∅) → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
87ex 399 . . . . . . . 8 (𝑏𝐵 → (Pred(𝑅, 𝐵, 𝑏) = ∅ → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
98adantl 469 . . . . . . 7 (((𝑅 Fr 𝐵𝑅 Se 𝐵) ∧ 𝑏𝐵) → (Pred(𝑅, 𝐵, 𝑏) = ∅ → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
10 setlikespec 5908 . . . . . . . . . . 11 ((𝑏𝐵𝑅 Se 𝐵) → Pred(𝑅, 𝐵, 𝑏) ∈ V)
11 trpredpred 32042 . . . . . . . . . . . . 13 (Pred(𝑅, 𝐵, 𝑏) ∈ V → Pred(𝑅, 𝐵, 𝑏) ⊆ TrPred(𝑅, 𝐵, 𝑏))
12 ssn0 4168 . . . . . . . . . . . . . 14 ((Pred(𝑅, 𝐵, 𝑏) ⊆ TrPred(𝑅, 𝐵, 𝑏) ∧ Pred(𝑅, 𝐵, 𝑏) ≠ ∅) → TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)
1312ex 399 . . . . . . . . . . . . 13 (Pred(𝑅, 𝐵, 𝑏) ⊆ TrPred(𝑅, 𝐵, 𝑏) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → TrPred(𝑅, 𝐵, 𝑏) ≠ ∅))
1411, 13syl 17 . . . . . . . . . . . 12 (Pred(𝑅, 𝐵, 𝑏) ∈ V → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → TrPred(𝑅, 𝐵, 𝑏) ≠ ∅))
15 trpredss 32043 . . . . . . . . . . . 12 (Pred(𝑅, 𝐵, 𝑏) ∈ V → TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵)
1614, 15jctild 517 . . . . . . . . . . 11 (Pred(𝑅, 𝐵, 𝑏) ∈ V → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)))
1710, 16syl 17 . . . . . . . . . 10 ((𝑏𝐵𝑅 Se 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)))
1817adantr 468 . . . . . . . . 9 (((𝑏𝐵𝑅 Se 𝐵) ∧ 𝑅 Fr 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)))
19 trpredex 32051 . . . . . . . . . . 11 TrPred(𝑅, 𝐵, 𝑏) ∈ V
20 sseq1 3817 . . . . . . . . . . . . . 14 (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (𝑐𝐵 ↔ TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵))
21 neeq1 3036 . . . . . . . . . . . . . 14 (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (𝑐 ≠ ∅ ↔ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅))
2220, 21anbi12d 618 . . . . . . . . . . . . 13 (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → ((𝑐𝐵𝑐 ≠ ∅) ↔ (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)))
23 predeq2 5890 . . . . . . . . . . . . . . 15 (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → Pred(𝑅, 𝑐, 𝑦) = Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦))
2423eqeq1d 2804 . . . . . . . . . . . . . 14 (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (Pred(𝑅, 𝑐, 𝑦) = ∅ ↔ Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅))
2524rexeqbi1dv 3332 . . . . . . . . . . . . 13 (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (∃𝑦𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅ ↔ ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅))
2622, 25imbi12d 335 . . . . . . . . . . . 12 (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (((𝑐𝐵𝑐 ≠ ∅) → ∃𝑦𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅) ↔ ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅)))
2726imbi2d 331 . . . . . . . . . . 11 (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → ((𝑅 Fr 𝐵 → ((𝑐𝐵𝑐 ≠ ∅) → ∃𝑦𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅)) ↔ (𝑅 Fr 𝐵 → ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅))))
28 dffr4 5903 . . . . . . . . . . . 12 (𝑅 Fr 𝐵 ↔ ∀𝑐((𝑐𝐵𝑐 ≠ ∅) → ∃𝑦𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅))
29 sp 2217 . . . . . . . . . . . 12 (∀𝑐((𝑐𝐵𝑐 ≠ ∅) → ∃𝑦𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅) → ((𝑐𝐵𝑐 ≠ ∅) → ∃𝑦𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅))
3028, 29sylbi 208 . . . . . . . . . . 11 (𝑅 Fr 𝐵 → ((𝑐𝐵𝑐 ≠ ∅) → ∃𝑦𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅))
3119, 27, 30vtocl 3448 . . . . . . . . . 10 (𝑅 Fr 𝐵 → ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅))
3210, 15syl 17 . . . . . . . . . . 11 ((𝑏𝐵𝑅 Se 𝐵) → TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵)
3332adantr 468 . . . . . . . . . . . . . . 15 (((𝑏𝐵𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵)
34 trpredtr 32044 . . . . . . . . . . . . . . . 16 ((𝑏𝐵𝑅 Se 𝐵) → (𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏) → Pred(𝑅, 𝐵, 𝑦) ⊆ TrPred(𝑅, 𝐵, 𝑏)))
3534imp 395 . . . . . . . . . . . . . . 15 (((𝑏𝐵𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → Pred(𝑅, 𝐵, 𝑦) ⊆ TrPred(𝑅, 𝐵, 𝑏))
36 sspred 5895 . . . . . . . . . . . . . . 15 ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(𝑅, 𝐵, 𝑦) ⊆ TrPred(𝑅, 𝐵, 𝑏)) → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦))
3733, 35, 36syl2anc 575 . . . . . . . . . . . . . 14 (((𝑏𝐵𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦))
3837eqeq1d 2804 . . . . . . . . . . . . 13 (((𝑏𝐵𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → (Pred(𝑅, 𝐵, 𝑦) = ∅ ↔ Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅))
3938biimprd 239 . . . . . . . . . . . 12 (((𝑏𝐵𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → (Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅ → Pred(𝑅, 𝐵, 𝑦) = ∅))
4039reximdva 3200 . . . . . . . . . . 11 ((𝑏𝐵𝑅 Se 𝐵) → (∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅ → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, 𝐵, 𝑦) = ∅))
41 ssrexv 3858 . . . . . . . . . . 11 (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 → (∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, 𝐵, 𝑦) = ∅ → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
4232, 40, 41sylsyld 61 . . . . . . . . . 10 ((𝑏𝐵𝑅 Se 𝐵) → (∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅ → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
4331, 42sylan9r 500 . . . . . . . . 9 (((𝑏𝐵𝑅 Se 𝐵) ∧ 𝑅 Fr 𝐵) → ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
4418, 43syld 47 . . . . . . . 8 (((𝑏𝐵𝑅 Se 𝐵) ∧ 𝑅 Fr 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
4544an31s 636 . . . . . . 7 (((𝑅 Fr 𝐵𝑅 Se 𝐵) ∧ 𝑏𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
469, 45pm2.61dne 3060 . . . . . 6 (((𝑅 Fr 𝐵𝑅 Se 𝐵) ∧ 𝑏𝐵) → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
4746ex 399 . . . . 5 ((𝑅 Fr 𝐵𝑅 Se 𝐵) → (𝑏𝐵 → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
4847exlimdv 2023 . . . 4 ((𝑅 Fr 𝐵𝑅 Se 𝐵) → (∃𝑏 𝑏𝐵 → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
494, 48syl5bi 233 . . 3 ((𝑅 Fr 𝐵𝑅 Se 𝐵) → (𝐵 ≠ ∅ → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))
503, 49syl6com 37 . 2 ((𝑅 Fr 𝐴𝑅 Se 𝐴) → (𝐵𝐴 → (𝐵 ≠ ∅ → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)))
5150imp32 407 1 (((𝑅 Fr 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1635   = wceq 1637  wex 1859  wcel 2155  wne 2974  wrex 3093  Vcvv 3387  wss 3763  c0 4110   Fr wfr 5261   Se wse 5262  Predcpred 5886  TrPredctrpred 32031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-inf2 8779
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-reu 3099  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-se 5265  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-om 7290  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-trpred 32032
This theorem is referenced by:  frind  32058
  Copyright terms: Public domain W3C validator