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

Theorem wefrc 5542
Description: A nonempty subclass of a class well-ordered by membership has a minimal element. Special case of Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by NM, 17-Feb-2004.)
Assertion
Ref Expression
wefrc (( E We 𝐴𝐵𝐴𝐵 ≠ ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
Distinct variable group:   𝑥,𝐵
Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem wefrc
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wess 5535 . . 3 (𝐵𝐴 → ( E We 𝐴 → E We 𝐵))
2 n0 4307 . . . 4 (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦𝐵)
3 ineq2 4180 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐵𝑥) = (𝐵𝑦))
43eqeq1d 2820 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝐵𝑥) = ∅ ↔ (𝐵𝑦) = ∅))
54rspcev 3620 . . . . . . . . 9 ((𝑦𝐵 ∧ (𝐵𝑦) = ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
65ex 413 . . . . . . . 8 (𝑦𝐵 → ((𝐵𝑦) = ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
76adantl 482 . . . . . . 7 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) = ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
8 inss1 4202 . . . . . . . . . . 11 (𝐵𝑦) ⊆ 𝐵
9 wefr 5538 . . . . . . . . . . . . 13 ( E We 𝐵 → E Fr 𝐵)
10 vex 3495 . . . . . . . . . . . . . . 15 𝑦 ∈ V
1110inex2 5213 . . . . . . . . . . . . . 14 (𝐵𝑦) ∈ V
1211epfrc 5534 . . . . . . . . . . . . 13 (( E Fr 𝐵 ∧ (𝐵𝑦) ⊆ 𝐵 ∧ (𝐵𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)
139, 12syl3an1 1155 . . . . . . . . . . . 12 (( E We 𝐵 ∧ (𝐵𝑦) ⊆ 𝐵 ∧ (𝐵𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)
14133exp 1111 . . . . . . . . . . 11 ( E We 𝐵 → ((𝐵𝑦) ⊆ 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)))
158, 14mpi 20 . . . . . . . . . 10 ( E We 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅))
16 rexin 4213 . . . . . . . . . 10 (∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅ ↔ ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅))
1715, 16syl6ib 252 . . . . . . . . 9 ( E We 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
1817adantr 481 . . . . . . . 8 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
19 elin 4166 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐵𝑥) ↔ (𝑧𝐵𝑧𝑥))
20 df-3an 1081 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐵𝑧𝐵𝑥𝐵) ↔ ((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵))
21 3anrot 1092 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐵𝑧𝐵𝑥𝐵) ↔ (𝑧𝐵𝑥𝐵𝑦𝐵))
2220, 21bitr3i 278 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵) ↔ (𝑧𝐵𝑥𝐵𝑦𝐵))
23 wetrep 5541 . . . . . . . . . . . . . . . . . . . . . . 23 (( E We 𝐵 ∧ (𝑧𝐵𝑥𝐵𝑦𝐵)) → ((𝑧𝑥𝑥𝑦) → 𝑧𝑦))
2423expd 416 . . . . . . . . . . . . . . . . . . . . . 22 (( E We 𝐵 ∧ (𝑧𝐵𝑥𝐵𝑦𝐵)) → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))
2522, 24sylan2b 593 . . . . . . . . . . . . . . . . . . . . 21 (( E We 𝐵 ∧ ((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵)) → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))
2625exp44 438 . . . . . . . . . . . . . . . . . . . 20 ( E We 𝐵 → (𝑦𝐵 → (𝑧𝐵 → (𝑥𝐵 → (𝑧𝑥 → (𝑥𝑦𝑧𝑦))))))
2726imp 407 . . . . . . . . . . . . . . . . . . 19 (( E We 𝐵𝑦𝐵) → (𝑧𝐵 → (𝑥𝐵 → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))))
2827com34 91 . . . . . . . . . . . . . . . . . 18 (( E We 𝐵𝑦𝐵) → (𝑧𝐵 → (𝑧𝑥 → (𝑥𝐵 → (𝑥𝑦𝑧𝑦)))))
2928impd 411 . . . . . . . . . . . . . . . . 17 (( E We 𝐵𝑦𝐵) → ((𝑧𝐵𝑧𝑥) → (𝑥𝐵 → (𝑥𝑦𝑧𝑦))))
3019, 29syl5bi 243 . . . . . . . . . . . . . . . 16 (( E We 𝐵𝑦𝐵) → (𝑧 ∈ (𝐵𝑥) → (𝑥𝐵 → (𝑥𝑦𝑧𝑦))))
3130imp4a 423 . . . . . . . . . . . . . . 15 (( E We 𝐵𝑦𝐵) → (𝑧 ∈ (𝐵𝑥) → ((𝑥𝐵𝑥𝑦) → 𝑧𝑦)))
3231com23 86 . . . . . . . . . . . . . 14 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (𝑧 ∈ (𝐵𝑥) → 𝑧𝑦)))
3332ralrimdv 3185 . . . . . . . . . . . . 13 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → ∀𝑧 ∈ (𝐵𝑥)𝑧𝑦))
34 dfss3 3953 . . . . . . . . . . . . 13 ((𝐵𝑥) ⊆ 𝑦 ↔ ∀𝑧 ∈ (𝐵𝑥)𝑧𝑦)
3533, 34syl6ibr 253 . . . . . . . . . . . 12 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (𝐵𝑥) ⊆ 𝑦))
36 dfss 3950 . . . . . . . . . . . . . . 15 ((𝐵𝑥) ⊆ 𝑦 ↔ (𝐵𝑥) = ((𝐵𝑥) ∩ 𝑦))
37 in32 4195 . . . . . . . . . . . . . . . 16 ((𝐵𝑥) ∩ 𝑦) = ((𝐵𝑦) ∩ 𝑥)
3837eqeq2i 2831 . . . . . . . . . . . . . . 15 ((𝐵𝑥) = ((𝐵𝑥) ∩ 𝑦) ↔ (𝐵𝑥) = ((𝐵𝑦) ∩ 𝑥))
3936, 38sylbb 220 . . . . . . . . . . . . . 14 ((𝐵𝑥) ⊆ 𝑦 → (𝐵𝑥) = ((𝐵𝑦) ∩ 𝑥))
4039eqeq1d 2820 . . . . . . . . . . . . 13 ((𝐵𝑥) ⊆ 𝑦 → ((𝐵𝑥) = ∅ ↔ ((𝐵𝑦) ∩ 𝑥) = ∅))
4140biimprd 249 . . . . . . . . . . . 12 ((𝐵𝑥) ⊆ 𝑦 → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅))
4235, 41syl6 35 . . . . . . . . . . 11 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅)))
4342expd 416 . . . . . . . . . 10 (( E We 𝐵𝑦𝐵) → (𝑥𝐵 → (𝑥𝑦 → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅))))
4443imp4a 423 . . . . . . . . 9 (( E We 𝐵𝑦𝐵) → (𝑥𝐵 → ((𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) → (𝐵𝑥) = ∅)))
4544reximdvai 3269 . . . . . . . 8 (( E We 𝐵𝑦𝐵) → (∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅))
4618, 45syld 47 . . . . . . 7 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
477, 46pm2.61dne 3100 . . . . . 6 (( E We 𝐵𝑦𝐵) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
4847ex 413 . . . . 5 ( E We 𝐵 → (𝑦𝐵 → ∃𝑥𝐵 (𝐵𝑥) = ∅))
4948exlimdv 1925 . . . 4 ( E We 𝐵 → (∃𝑦 𝑦𝐵 → ∃𝑥𝐵 (𝐵𝑥) = ∅))
502, 49syl5bi 243 . . 3 ( E We 𝐵 → (𝐵 ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
511, 50syl6com 37 . 2 ( E We 𝐴 → (𝐵𝐴 → (𝐵 ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅)))
52513imp 1103 1 (( E We 𝐴𝐵𝐴𝐵 ≠ ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079   = wceq 1528  wex 1771  wcel 2105  wne 3013  wral 3135  wrex 3136  cin 3932  wss 3933  c0 4288   E cep 5457   Fr wfr 5504   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  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  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-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-opab 5120  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509
This theorem is referenced by:  tz7.5  6205  onnseq  7970  finminlem  33563
  Copyright terms: Public domain W3C validator