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

Theorem wereu2 5545
Description: All nonempty subclasses of a class having a well-ordered and set-like relation have a minimal element for that relation. 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 4307 . . . 4 (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧𝐵)
2 rabeq0 4335 . . . . . . . 8 ({𝑤𝐵𝑤𝑅𝑧} = ∅ ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧)
3 breq1 5060 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦𝑅𝑥𝑤𝑅𝑥))
43notbid 319 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑤𝑅𝑥))
54cbvralvw 3447 . . . . . . . . . . . 12 (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑥)
6 breq2 5061 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑤𝑅𝑥𝑤𝑅𝑧))
76notbid 319 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (¬ 𝑤𝑅𝑥 ↔ ¬ 𝑤𝑅𝑧))
87ralbidv 3194 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (∀𝑤𝐵 ¬ 𝑤𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
95, 8syl5bb 284 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
109rspcev 3620 . . . . . . . . . 10 ((𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
1110ex 413 . . . . . . . . 9 (𝑧𝐵 → (∀𝑤𝐵 ¬ 𝑤𝑅𝑧 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
1211ad2antll 725 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∀𝑤𝐵 ¬ 𝑤𝑅𝑧 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
132, 12syl5bi 243 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} = ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
14 simprl 767 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝐵𝐴)
15 simplr 765 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Se 𝐴)
16 sess2 5517 . . . . . . . . . . 11 (𝐵𝐴 → (𝑅 Se 𝐴𝑅 Se 𝐵))
1714, 15, 16sylc 65 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Se 𝐵)
18 simprr 769 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑧𝐵)
19 seex 5511 . . . . . . . . . 10 ((𝑅 Se 𝐵𝑧𝐵) → {𝑤𝐵𝑤𝑅𝑧} ∈ V)
2017, 18, 19syl2anc 584 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → {𝑤𝐵𝑤𝑅𝑧} ∈ V)
21 wefr 5538 . . . . . . . . . 10 (𝑅 We 𝐴𝑅 Fr 𝐴)
2221ad2antrr 722 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Fr 𝐴)
23 ssrab2 4053 . . . . . . . . . 10 {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐵
2423, 14sstrid 3975 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴)
25 fri 5510 . . . . . . . . . 10 ((({𝑤𝐵𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴 ∧ {𝑤𝐵𝑤𝑅𝑧} ≠ ∅)) → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥)
2625expr 457 . . . . . . . . 9 ((({𝑤𝐵𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
2720, 22, 24, 26syl21anc 833 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
28 breq1 5060 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝑤𝑅𝑧𝑥𝑅𝑧))
2928rexrab 3684 . . . . . . . . 9 (∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∃𝑥𝐵 (𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
30 breq1 5060 . . . . . . . . . . . . 13 (𝑤 = 𝑦 → (𝑤𝑅𝑧𝑦𝑅𝑧))
3130ralrab 3682 . . . . . . . . . . . 12 (∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∀𝑦𝐵 (𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥))
32 weso 5539 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 We 𝐴𝑅 Or 𝐴)
3332ad2antrr 722 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Or 𝐴)
34 soss 5486 . . . . . . . . . . . . . . . . . . . . 21 (𝐵𝐴 → (𝑅 Or 𝐴𝑅 Or 𝐵))
3514, 33, 34sylc 65 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Or 𝐵)
3635ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑅 Or 𝐵)
37 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑦𝐵)
38 simplr 765 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑥𝐵)
3918ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑧𝐵)
40 sotr 5490 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐵 ∧ (𝑦𝐵𝑥𝐵𝑧𝐵)) → ((𝑦𝑅𝑥𝑥𝑅𝑧) → 𝑦𝑅𝑧))
4136, 37, 38, 39, 40syl13anc 1364 . . . . . . . . . . . . . . . . . 18 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ((𝑦𝑅𝑥𝑥𝑅𝑧) → 𝑦𝑅𝑧))
4241ancomsd 466 . . . . . . . . . . . . . . . . 17 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ((𝑥𝑅𝑧𝑦𝑅𝑥) → 𝑦𝑅𝑧))
4342expdimp 453 . . . . . . . . . . . . . . . 16 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝑅𝑧) → (𝑦𝑅𝑥𝑦𝑅𝑧))
4443an32s 648 . . . . . . . . . . . . . . 15 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (𝑦𝑅𝑥𝑦𝑅𝑧))
4544con3d 155 . . . . . . . . . . . . . 14 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (¬ 𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥))
46 idd 24 . . . . . . . . . . . . . 14 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (¬ 𝑦𝑅𝑥 → ¬ 𝑦𝑅𝑥))
4745, 46jad 188 . . . . . . . . . . . . 13 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → ((𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥) → ¬ 𝑦𝑅𝑥))
4847ralimdva 3174 . . . . . . . . . . . 12 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) → (∀𝑦𝐵 (𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥) → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
4931, 48syl5bi 243 . . . . . . . . . . 11 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) → (∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
5049expimpd 454 . . . . . . . . . 10 ((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) → ((𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥) → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
5150reximdva 3271 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∃𝑥𝐵 (𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5229, 51syl5bi 243 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5327, 52syld 47 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5413, 53pm2.61dne 3100 . . . . . 6 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
5554expr 457 . . . . 5 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (𝑧𝐵 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5655exlimdv 1925 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (∃𝑧 𝑧𝐵 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
571, 56syl5bi 243 . . 3 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (𝐵 ≠ ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5857impr 455 . 2 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
59 simprl 767 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵𝐴)
6032ad2antrr 722 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Or 𝐴)
6159, 60, 34sylc 65 . . 3 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Or 𝐵)
62 somo 5503 . . 3 (𝑅 Or 𝐵 → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
6361, 62syl 17 . 2 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
64 reu5 3428 . 2 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
6558, 63, 64sylanbrc 583 1 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1528  wex 1771  wcel 2105  wne 3013  wral 3135  wrex 3136  ∃!wreu 3137  ∃*wrmo 3138  {crab 3139  Vcvv 3492  wss 3933  c0 4288   class class class wbr 5057   Or wor 5466   Fr wfr 5504   Se wse 5505   We wwe 5506
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509
This theorem is referenced by:  tz6.26  6172  weniso  7096  ordtypelem3  8972  dfac8clem  9446
  Copyright terms: Public domain W3C validator