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

Theorem wereu2 5140
Description: All nonempty (possibly proper) subclasses of 𝐴, which has a well-founded relation 𝑅, have 𝑅-minimal elements. 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 3964 . . . 4 (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧𝐵)
2 rabeq0 3990 . . . . . . . 8 ({𝑤𝐵𝑤𝑅𝑧} = ∅ ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧)
3 breq1 4688 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦𝑅𝑥𝑤𝑅𝑥))
43notbid 307 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑤𝑅𝑥))
54cbvralv 3201 . . . . . . . . . . . 12 (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑥)
6 breq2 4689 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑤𝑅𝑥𝑤𝑅𝑧))
76notbid 307 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (¬ 𝑤𝑅𝑥 ↔ ¬ 𝑤𝑅𝑧))
87ralbidv 3015 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (∀𝑤𝐵 ¬ 𝑤𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
95, 8syl5bb 272 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧))
109rspcev 3340 . . . . . . . . . 10 ((𝑧𝐵 ∧ ∀𝑤𝐵 ¬ 𝑤𝑅𝑧) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
1110ex 449 . . . . . . . . 9 (𝑧𝐵 → (∀𝑤𝐵 ¬ 𝑤𝑅𝑧 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
1211ad2antll 765 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∀𝑤𝐵 ¬ 𝑤𝑅𝑧 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
132, 12syl5bi 232 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} = ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
14 simprl 809 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝐵𝐴)
15 simplr 807 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Se 𝐴)
16 sess2 5112 . . . . . . . . . . 11 (𝐵𝐴 → (𝑅 Se 𝐴𝑅 Se 𝐵))
1714, 15, 16sylc 65 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Se 𝐵)
18 simprr 811 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑧𝐵)
19 seex 5106 . . . . . . . . . 10 ((𝑅 Se 𝐵𝑧𝐵) → {𝑤𝐵𝑤𝑅𝑧} ∈ V)
2017, 18, 19syl2anc 694 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → {𝑤𝐵𝑤𝑅𝑧} ∈ V)
21 wefr 5133 . . . . . . . . . 10 (𝑅 We 𝐴𝑅 Fr 𝐴)
2221ad2antrr 762 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Fr 𝐴)
23 ssrab2 3720 . . . . . . . . . 10 {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐵
2423, 14syl5ss 3647 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴)
25 fri 5105 . . . . . . . . . 10 ((({𝑤𝐵𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴 ∧ {𝑤𝐵𝑤𝑅𝑧} ≠ ∅)) → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥)
2625expr 642 . . . . . . . . 9 ((({𝑤𝐵𝑤𝑅𝑧} ∈ V ∧ 𝑅 Fr 𝐴) ∧ {𝑤𝐵𝑤𝑅𝑧} ⊆ 𝐴) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
2720, 22, 24, 26syl21anc 1365 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
28 breq1 4688 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝑤𝑅𝑧𝑥𝑅𝑧))
2928rexrab 3403 . . . . . . . . 9 (∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∃𝑥𝐵 (𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥))
30 breq1 4688 . . . . . . . . . . . . 13 (𝑤 = 𝑦 → (𝑤𝑅𝑧𝑦𝑅𝑧))
3130ralrab 3401 . . . . . . . . . . . 12 (∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 ↔ ∀𝑦𝐵 (𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥))
32 weso 5134 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 We 𝐴𝑅 Or 𝐴)
3332ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Or 𝐴)
34 soss 5082 . . . . . . . . . . . . . . . . . . . . 21 (𝐵𝐴 → (𝑅 Or 𝐴𝑅 Or 𝐵))
3514, 33, 34sylc 65 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → 𝑅 Or 𝐵)
3635ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑅 Or 𝐵)
37 simpr 476 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑦𝐵)
38 simplr 807 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑥𝐵)
3918ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑧𝐵)
40 sotr 5086 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐵 ∧ (𝑦𝐵𝑥𝐵𝑧𝐵)) → ((𝑦𝑅𝑥𝑥𝑅𝑧) → 𝑦𝑅𝑧))
4136, 37, 38, 39, 40syl13anc 1368 . . . . . . . . . . . . . . . . . 18 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ((𝑦𝑅𝑥𝑥𝑅𝑧) → 𝑦𝑅𝑧))
4241ancomsd 469 . . . . . . . . . . . . . . . . 17 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ((𝑥𝑅𝑧𝑦𝑅𝑥) → 𝑦𝑅𝑧))
4342expdimp 452 . . . . . . . . . . . . . . . 16 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑦𝐵) ∧ 𝑥𝑅𝑧) → (𝑦𝑅𝑥𝑦𝑅𝑧))
4443an32s 863 . . . . . . . . . . . . . . 15 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (𝑦𝑅𝑥𝑦𝑅𝑧))
4544con3d 148 . . . . . . . . . . . . . 14 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (¬ 𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥))
46 idd 24 . . . . . . . . . . . . . 14 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → (¬ 𝑦𝑅𝑥 → ¬ 𝑦𝑅𝑥))
4745, 46jad 174 . . . . . . . . . . . . 13 ((((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) ∧ 𝑦𝐵) → ((𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥) → ¬ 𝑦𝑅𝑥))
4847ralimdva 2991 . . . . . . . . . . . 12 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) → (∀𝑦𝐵 (𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑥) → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
4931, 48syl5bi 232 . . . . . . . . . . 11 (((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) ∧ 𝑥𝑅𝑧) → (∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
5049expimpd 628 . . . . . . . . . 10 ((((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) ∧ 𝑥𝐵) → ((𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥) → ∀𝑦𝐵 ¬ 𝑦𝑅𝑥))
5150reximdva 3046 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∃𝑥𝐵 (𝑥𝑅𝑧 ∧ ∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5229, 51syl5bi 232 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → (∃𝑥 ∈ {𝑤𝐵𝑤𝑅𝑧}∀𝑦 ∈ {𝑤𝐵𝑤𝑅𝑧} ¬ 𝑦𝑅𝑥 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5327, 52syld 47 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ({𝑤𝐵𝑤𝑅𝑧} ≠ ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5413, 53pm2.61dne 2909 . . . . . 6 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝑧𝐵)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
5554expr 642 . . . . 5 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (𝑧𝐵 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5655exlimdv 1901 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (∃𝑧 𝑧𝐵 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
571, 56syl5bi 232 . . 3 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝐵𝐴) → (𝐵 ≠ ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
5857impr 648 . 2 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
59 simprl 809 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝐵𝐴)
6032ad2antrr 762 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Or 𝐴)
6159, 60, 34sylc 65 . . 3 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Or 𝐵)
62 somo 5098 . . 3 (𝑅 Or 𝐵 → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
6361, 62syl 17 . 2 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
64 reu5 3189 . 2 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))
6558, 63, 64sylanbrc 699 1 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1523  wex 1744  wcel 2030  wne 2823  wral 2941  wrex 2942  ∃!wreu 2943  ∃*wrmo 2944  {crab 2945  Vcvv 3231  wss 3607  c0 3948   class class class wbr 4685   Or wor 5063   Fr wfr 5099   Se wse 5100   We wwe 5101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104
This theorem is referenced by:  tz6.26  5749  weniso  6644  ordtypelem3  8466  dfac8clem  8893
  Copyright terms: Public domain W3C validator