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

Theorem wereu2 5686
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 4359 . . . 4 (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧𝐵)
2 rabeq0 4394 . . . . . . . 8 ({𝑤𝐵𝑤𝑅𝑧} = ∅ ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧)
3 breq1 5151 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦𝑅𝑥𝑤𝑅𝑥))
43notbid 318 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑤𝑅𝑥))
54cbvralvw 3235 . . . . . . . . . . . 12 (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑥)
6 breq2 5152 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑤𝑅𝑥𝑤𝑅𝑧))
76notbid 318 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (¬ 𝑤𝑅𝑥 ↔ ¬ 𝑤𝑅𝑧))
87ralbidv 3176 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (∀𝑤𝐵 ¬ 𝑤𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
95, 8bitrid 283 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
109rspcev 3622 . . . . . . . . . 10 ((𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
1110ex 412 . . . . . . . . 9 (𝑧𝐵 → (∀𝑤𝐵 ¬ 𝑤𝑅𝑧 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
1211ad2antll 729 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∀𝑤𝐵 ¬ 𝑤𝑅𝑧 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
132, 12biimtrid 242 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} = ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
14 simprl 771 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝐵𝐴)
15 simplr 769 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Se 𝐴)
16 sess2 5655 . . . . . . . . . . 11 (𝐵𝐴 → (𝑅 Se 𝐴𝑅 Se 𝐵))
1714, 15, 16sylc 65 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Se 𝐵)
18 simprr 773 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑧𝐵)
19 seex 5648 . . . . . . . . . 10 ((𝑅 Se 𝐵𝑧𝐵) → {𝑤𝐵𝑤𝑅𝑧} ∈ V)
2017, 18, 19syl2anc 584 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → {𝑤𝐵𝑤𝑅𝑧} ∈ V)
21 wefr 5679 . . . . . . . . . 10 (𝑅 We 𝐴𝑅 Fr 𝐴)
2221ad2antrr 726 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Fr 𝐴)
23 ssrab2 4090 . . . . . . . . . 10 {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐵
2423, 14sstrid 4007 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴)
25 fri 5646 . . . . . . . . . 10 ((({𝑤𝐵𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴 ∧ {𝑤𝐵𝑤𝑅𝑧} ≠ ∅)) → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥)
2625expr 456 . . . . . . . . 9 ((({𝑤𝐵𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
2720, 22, 24, 26syl21anc 838 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
28 breq1 5151 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝑤𝑅𝑧𝑥𝑅𝑧))
2928rexrab 3705 . . . . . . . . 9 (∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∃𝑥𝐵 (𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
30 breq1 5151 . . . . . . . . . . . . 13 (𝑤 = 𝑦 → (𝑤𝑅𝑧𝑦𝑅𝑧))
3130ralrab 3702 . . . . . . . . . . . 12 (∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∀𝑦𝐵 (𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥))
32 weso 5680 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 We 𝐴𝑅 Or 𝐴)
3332ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Or 𝐴)
34 soss 5617 . . . . . . . . . . . . . . . . . . . . 21 (𝐵𝐴 → (𝑅 Or 𝐴𝑅 Or 𝐵))
3514, 33, 34sylc 65 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Or 𝐵)
3635ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑅 Or 𝐵)
37 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑦𝐵)
38 simplr 769 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑥𝐵)
3918ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑧𝐵)
40 sotr 5622 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐵 ∧ (𝑦𝐵𝑥𝐵𝑧𝐵)) → ((𝑦𝑅𝑥𝑥𝑅𝑧) → 𝑦𝑅𝑧))
4136, 37, 38, 39, 40syl13anc 1371 . . . . . . . . . . . . . . . . . 18 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ((𝑦𝑅𝑥𝑥𝑅𝑧) → 𝑦𝑅𝑧))
4241ancomsd 465 . . . . . . . . . . . . . . . . 17 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ((𝑥𝑅𝑧𝑦𝑅𝑥) → 𝑦𝑅𝑧))
4342expdimp 452 . . . . . . . . . . . . . . . 16 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝑅𝑧) → (𝑦𝑅𝑥𝑦𝑅𝑧))
4443an32s 652 . . . . . . . . . . . . . . 15 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (𝑦𝑅𝑥𝑦𝑅𝑧))
4544con3d 152 . . . . . . . . . . . . . 14 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (¬ 𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥))
46 idd 24 . . . . . . . . . . . . . 14 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (¬ 𝑦𝑅𝑥 → ¬ 𝑦𝑅𝑥))
4745, 46jad 187 . . . . . . . . . . . . 13 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → ((𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥) → ¬ 𝑦𝑅𝑥))
4847ralimdva 3165 . . . . . . . . . . . 12 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) → (∀𝑦𝐵 (𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥) → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
4931, 48biimtrid 242 . . . . . . . . . . 11 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) → (∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
5049expimpd 453 . . . . . . . . . 10 ((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) → ((𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥) → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
5150reximdva 3166 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∃𝑥𝐵 (𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5229, 51biimtrid 242 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5327, 52syld 47 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5413, 53pm2.61dne 3026 . . . . . 6 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
5554expr 456 . . . . 5 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (𝑧𝐵 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5655exlimdv 1931 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (∃𝑧 𝑧𝐵 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
571, 56biimtrid 242 . . 3 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (𝐵 ≠ ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5857impr 454 . 2 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
59 simprl 771 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵𝐴)
6032ad2antrr 726 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Or 𝐴)
6159, 60, 34sylc 65 . . 3 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Or 𝐵)
62 somo 5635 . . 3 (𝑅 Or 𝐵 → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
6361, 62syl 17 . 2 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
64 reu5 3380 . 2 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
6558, 63, 64sylanbrc 583 1 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1537  wex 1776  wcel 2106  wne 2938  wral 3059  wrex 3068  ∃!wreu 3376  ∃*wrmo 3377  {crab 3433  Vcvv 3478  wss 3963  c0 4339   class class class wbr 5148   Or wor 5596   Fr wfr 5638   Se wse 5639   We wwe 5640
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643
This theorem is referenced by:  tz6.26OLD  6371  weniso  7374  ordtypelem3  9558  dfac8clem  10070  weiunlem2  36446  weiunfrlem  36447
  Copyright terms: Public domain W3C validator