MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wereu2 Structured version   Visualization version   GIF version

Theorem wereu2 5673
Description: A nonempty subclass of an 𝑅-well-ordered and 𝑅-setlike class has a unique 𝑅-minimal element. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 24-Jun-2015.)
Assertion
Ref Expression
wereu2 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦

Proof of Theorem wereu2
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0 4346 . . . 4 (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧𝐵)
2 rabeq0 4384 . . . . . . . 8 ({𝑤𝐵𝑤𝑅𝑧} = ∅ ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧)
3 breq1 5151 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦𝑅𝑥𝑤𝑅𝑥))
43notbid 318 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑤𝑅𝑥))
54cbvralvw 3235 . . . . . . . . . . . 12 (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑥)
6 breq2 5152 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑤𝑅𝑥𝑤𝑅𝑧))
76notbid 318 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (¬ 𝑤𝑅𝑥 ↔ ¬ 𝑤𝑅𝑧))
87ralbidv 3178 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (∀𝑤𝐵 ¬ 𝑤𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
95, 8bitrid 283 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
109rspcev 3613 . . . . . . . . . 10 ((𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
1110ex 414 . . . . . . . . 9 (𝑧𝐵 → (∀𝑤𝐵 ¬ 𝑤𝑅𝑧 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
1211ad2antll 728 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∀𝑤𝐵 ¬ 𝑤𝑅𝑧 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
132, 12biimtrid 241 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} = ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
14 simprl 770 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝐵𝐴)
15 simplr 768 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Se 𝐴)
16 sess2 5645 . . . . . . . . . . 11 (𝐵𝐴 → (𝑅 Se 𝐴𝑅 Se 𝐵))
1714, 15, 16sylc 65 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Se 𝐵)
18 simprr 772 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑧𝐵)
19 seex 5638 . . . . . . . . . 10 ((𝑅 Se 𝐵𝑧𝐵) → {𝑤𝐵𝑤𝑅𝑧} ∈ V)
2017, 18, 19syl2anc 585 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → {𝑤𝐵𝑤𝑅𝑧} ∈ V)
21 wefr 5666 . . . . . . . . . 10 (𝑅 We 𝐴𝑅 Fr 𝐴)
2221ad2antrr 725 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Fr 𝐴)
23 ssrab2 4077 . . . . . . . . . 10 {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐵
2423, 14sstrid 3993 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴)
25 fri 5636 . . . . . . . . . 10 ((({𝑤𝐵𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴 ∧ {𝑤𝐵𝑤𝑅𝑧} ≠ ∅)) → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥)
2625expr 458 . . . . . . . . 9 ((({𝑤𝐵𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
2720, 22, 24, 26syl21anc 837 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
28 breq1 5151 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝑤𝑅𝑧𝑥𝑅𝑧))
2928rexrab 3692 . . . . . . . . 9 (∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∃𝑥𝐵 (𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
30 breq1 5151 . . . . . . . . . . . . 13 (𝑤 = 𝑦 → (𝑤𝑅𝑧𝑦𝑅𝑧))
3130ralrab 3689 . . . . . . . . . . . 12 (∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∀𝑦𝐵 (𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥))
32 weso 5667 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 We 𝐴𝑅 Or 𝐴)
3332ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Or 𝐴)
34 soss 5608 . . . . . . . . . . . . . . . . . . . . 21 (𝐵𝐴 → (𝑅 Or 𝐴𝑅 Or 𝐵))
3514, 33, 34sylc 65 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Or 𝐵)
3635ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑅 Or 𝐵)
37 simpr 486 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑦𝐵)
38 simplr 768 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑥𝐵)
3918ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑧𝐵)
40 sotr 5612 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐵 ∧ (𝑦𝐵𝑥𝐵𝑧𝐵)) → ((𝑦𝑅𝑥𝑥𝑅𝑧) → 𝑦𝑅𝑧))
4136, 37, 38, 39, 40syl13anc 1373 . . . . . . . . . . . . . . . . . 18 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ((𝑦𝑅𝑥𝑥𝑅𝑧) → 𝑦𝑅𝑧))
4241ancomsd 467 . . . . . . . . . . . . . . . . 17 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ((𝑥𝑅𝑧𝑦𝑅𝑥) → 𝑦𝑅𝑧))
4342expdimp 454 . . . . . . . . . . . . . . . 16 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝑅𝑧) → (𝑦𝑅𝑥𝑦𝑅𝑧))
4443an32s 651 . . . . . . . . . . . . . . 15 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (𝑦𝑅𝑥𝑦𝑅𝑧))
4544con3d 152 . . . . . . . . . . . . . 14 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (¬ 𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥))
46 idd 24 . . . . . . . . . . . . . 14 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (¬ 𝑦𝑅𝑥 → ¬ 𝑦𝑅𝑥))
4745, 46jad 187 . . . . . . . . . . . . 13 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → ((𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥) → ¬ 𝑦𝑅𝑥))
4847ralimdva 3168 . . . . . . . . . . . 12 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) → (∀𝑦𝐵 (𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥) → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
4931, 48biimtrid 241 . . . . . . . . . . 11 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) → (∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
5049expimpd 455 . . . . . . . . . 10 ((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) → ((𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥) → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
5150reximdva 3169 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∃𝑥𝐵 (𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5229, 51biimtrid 241 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5327, 52syld 47 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5413, 53pm2.61dne 3029 . . . . . 6 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
5554expr 458 . . . . 5 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (𝑧𝐵 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5655exlimdv 1937 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (∃𝑧 𝑧𝐵 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
571, 56biimtrid 241 . . 3 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (𝐵 ≠ ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5857impr 456 . 2 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
59 simprl 770 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵𝐴)
6032ad2antrr 725 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Or 𝐴)
6159, 60, 34sylc 65 . . 3 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Or 𝐵)
62 somo 5625 . . 3 (𝑅 Or 𝐵 → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
6361, 62syl 17 . 2 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
64 reu5 3379 . 2 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
6558, 63, 64sylanbrc 584 1 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  wex 1782  wcel 2107  wne 2941  wral 3062  wrex 3071  ∃!wreu 3375  ∃*wrmo 3376  {crab 3433  Vcvv 3475  wss 3948  c0 4322   class class class wbr 5148   Or wor 5587   Fr wfr 5628   Se wse 5629   We wwe 5630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633
This theorem is referenced by:  tz6.26OLD  6347  weniso  7348  ordtypelem3  9512  dfac8clem  10024
  Copyright terms: Public domain W3C validator