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

Theorem wereu2 5674
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 4347 . . . 4 (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧𝐵)
2 rabeq0 4385 . . . . . . . 8 ({𝑤𝐵𝑤𝑅𝑧} = ∅ ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧)
3 breq1 5152 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦𝑅𝑥𝑤𝑅𝑥))
43notbid 318 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑤𝑅𝑥))
54cbvralvw 3235 . . . . . . . . . . . 12 (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑥)
6 breq2 5153 . . . . . . . . . . . . . 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 5646 . . . . . . . . . . 11 (𝐵𝐴 → (𝑅 Se 𝐴𝑅 Se 𝐵))
1714, 15, 16sylc 65 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Se 𝐵)
18 simprr 772 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑧𝐵)
19 seex 5639 . . . . . . . . . 10 ((𝑅 Se 𝐵𝑧𝐵) → {𝑤𝐵𝑤𝑅𝑧} ∈ V)
2017, 18, 19syl2anc 585 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → {𝑤𝐵𝑤𝑅𝑧} ∈ V)
21 wefr 5667 . . . . . . . . . 10 (𝑅 We 𝐴𝑅 Fr 𝐴)
2221ad2antrr 725 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Fr 𝐴)
23 ssrab2 4078 . . . . . . . . . 10 {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐵
2423, 14sstrid 3994 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴)
25 fri 5637 . . . . . . . . . 10 ((({𝑤𝐵𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴 ∧ {𝑤𝐵𝑤𝑅𝑧} ≠ ∅)) → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥)
2625expr 458 . . . . . . . . 9 ((({𝑤𝐵𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
2720, 22, 24, 26syl21anc 837 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
28 breq1 5152 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝑤𝑅𝑧𝑥𝑅𝑧))
2928rexrab 3693 . . . . . . . . 9 (∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∃𝑥𝐵 (𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
30 breq1 5152 . . . . . . . . . . . . 13 (𝑤 = 𝑦 → (𝑤𝑅𝑧𝑦𝑅𝑧))
3130ralrab 3690 . . . . . . . . . . . 12 (∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∀𝑦𝐵 (𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥))
32 weso 5668 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 We 𝐴𝑅 Or 𝐴)
3332ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Or 𝐴)
34 soss 5609 . . . . . . . . . . . . . . . . . . . . 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 5613 . . . . . . . . . . . . . . . . . . 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 5626 . . 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 3949  c0 4323   class class class wbr 5149   Or wor 5588   Fr wfr 5629   Se wse 5630   We wwe 5631
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 5300
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 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634
This theorem is referenced by:  tz6.26OLD  6350  weniso  7351  ordtypelem3  9515  dfac8clem  10027
  Copyright terms: Public domain W3C validator