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

Theorem wefrc 5682
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 5674 . . 3 (𝐵𝐴 → ( E We 𝐴 → E We 𝐵))
2 n0 4358 . . . 4 (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦𝐵)
3 ineq2 4221 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐵𝑥) = (𝐵𝑦))
43eqeq1d 2736 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝐵𝑥) = ∅ ↔ (𝐵𝑦) = ∅))
54rspcev 3621 . . . . . . . . 9 ((𝑦𝐵 ∧ (𝐵𝑦) = ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
65ex 412 . . . . . . . 8 (𝑦𝐵 → ((𝐵𝑦) = ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
76adantl 481 . . . . . . 7 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) = ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
8 inss1 4244 . . . . . . . . . . 11 (𝐵𝑦) ⊆ 𝐵
9 wefr 5678 . . . . . . . . . . . . 13 ( E We 𝐵 → E Fr 𝐵)
10 vex 3481 . . . . . . . . . . . . . . 15 𝑦 ∈ V
1110inex2 5323 . . . . . . . . . . . . . 14 (𝐵𝑦) ∈ V
1211epfrc 5673 . . . . . . . . . . . . 13 (( E Fr 𝐵 ∧ (𝐵𝑦) ⊆ 𝐵 ∧ (𝐵𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)
139, 12syl3an1 1162 . . . . . . . . . . . 12 (( E We 𝐵 ∧ (𝐵𝑦) ⊆ 𝐵 ∧ (𝐵𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)
14133exp 1118 . . . . . . . . . . 11 ( E We 𝐵 → ((𝐵𝑦) ⊆ 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)))
158, 14mpi 20 . . . . . . . . . 10 ( E We 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅))
16 rexin 4255 . . . . . . . . . 10 (∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅ ↔ ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅))
1715, 16imbitrdi 251 . . . . . . . . 9 ( E We 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
1817adantr 480 . . . . . . . 8 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
19 elin 3978 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐵𝑥) ↔ (𝑧𝐵𝑧𝑥))
20 df-3an 1088 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐵𝑧𝐵𝑥𝐵) ↔ ((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵))
21 3anrot 1099 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐵𝑧𝐵𝑥𝐵) ↔ (𝑧𝐵𝑥𝐵𝑦𝐵))
2220, 21bitr3i 277 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵) ↔ (𝑧𝐵𝑥𝐵𝑦𝐵))
23 wetrep 5681 . . . . . . . . . . . . . . . . . . . . . . 23 (( E We 𝐵 ∧ (𝑧𝐵𝑥𝐵𝑦𝐵)) → ((𝑧𝑥𝑥𝑦) → 𝑧𝑦))
2423expd 415 . . . . . . . . . . . . . . . . . . . . . 22 (( E We 𝐵 ∧ (𝑧𝐵𝑥𝐵𝑦𝐵)) → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))
2522, 24sylan2b 594 . . . . . . . . . . . . . . . . . . . . 21 (( E We 𝐵 ∧ ((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵)) → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))
2625exp44 437 . . . . . . . . . . . . . . . . . . . 20 ( E We 𝐵 → (𝑦𝐵 → (𝑧𝐵 → (𝑥𝐵 → (𝑧𝑥 → (𝑥𝑦𝑧𝑦))))))
2726imp 406 . . . . . . . . . . . . . . . . . . 19 (( E We 𝐵𝑦𝐵) → (𝑧𝐵 → (𝑥𝐵 → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))))
2827com34 91 . . . . . . . . . . . . . . . . . 18 (( E We 𝐵𝑦𝐵) → (𝑧𝐵 → (𝑧𝑥 → (𝑥𝐵 → (𝑥𝑦𝑧𝑦)))))
2928impd 410 . . . . . . . . . . . . . . . . 17 (( E We 𝐵𝑦𝐵) → ((𝑧𝐵𝑧𝑥) → (𝑥𝐵 → (𝑥𝑦𝑧𝑦))))
3019, 29biimtrid 242 . . . . . . . . . . . . . . . 16 (( E We 𝐵𝑦𝐵) → (𝑧 ∈ (𝐵𝑥) → (𝑥𝐵 → (𝑥𝑦𝑧𝑦))))
3130imp4a 422 . . . . . . . . . . . . . . 15 (( E We 𝐵𝑦𝐵) → (𝑧 ∈ (𝐵𝑥) → ((𝑥𝐵𝑥𝑦) → 𝑧𝑦)))
3231com23 86 . . . . . . . . . . . . . 14 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (𝑧 ∈ (𝐵𝑥) → 𝑧𝑦)))
3332ralrimdv 3149 . . . . . . . . . . . . 13 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → ∀𝑧 ∈ (𝐵𝑥)𝑧𝑦))
34 dfss3 3983 . . . . . . . . . . . . 13 ((𝐵𝑥) ⊆ 𝑦 ↔ ∀𝑧 ∈ (𝐵𝑥)𝑧𝑦)
3533, 34imbitrrdi 252 . . . . . . . . . . . 12 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (𝐵𝑥) ⊆ 𝑦))
36 dfss 3981 . . . . . . . . . . . . . . 15 ((𝐵𝑥) ⊆ 𝑦 ↔ (𝐵𝑥) = ((𝐵𝑥) ∩ 𝑦))
37 in32 4237 . . . . . . . . . . . . . . . 16 ((𝐵𝑥) ∩ 𝑦) = ((𝐵𝑦) ∩ 𝑥)
3837eqeq2i 2747 . . . . . . . . . . . . . . 15 ((𝐵𝑥) = ((𝐵𝑥) ∩ 𝑦) ↔ (𝐵𝑥) = ((𝐵𝑦) ∩ 𝑥))
3936, 38sylbb 219 . . . . . . . . . . . . . 14 ((𝐵𝑥) ⊆ 𝑦 → (𝐵𝑥) = ((𝐵𝑦) ∩ 𝑥))
4039eqeq1d 2736 . . . . . . . . . . . . 13 ((𝐵𝑥) ⊆ 𝑦 → ((𝐵𝑥) = ∅ ↔ ((𝐵𝑦) ∩ 𝑥) = ∅))
4140biimprd 248 . . . . . . . . . . . 12 ((𝐵𝑥) ⊆ 𝑦 → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅))
4235, 41syl6 35 . . . . . . . . . . 11 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅)))
4342expd 415 . . . . . . . . . 10 (( E We 𝐵𝑦𝐵) → (𝑥𝐵 → (𝑥𝑦 → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅))))
4443imp4a 422 . . . . . . . . 9 (( E We 𝐵𝑦𝐵) → (𝑥𝐵 → ((𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) → (𝐵𝑥) = ∅)))
4544reximdvai 3162 . . . . . . . 8 (( E We 𝐵𝑦𝐵) → (∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅))
4618, 45syld 47 . . . . . . 7 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
477, 46pm2.61dne 3025 . . . . . 6 (( E We 𝐵𝑦𝐵) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
4847ex 412 . . . . 5 ( E We 𝐵 → (𝑦𝐵 → ∃𝑥𝐵 (𝐵𝑥) = ∅))
4948exlimdv 1930 . . . 4 ( E We 𝐵 → (∃𝑦 𝑦𝐵 → ∃𝑥𝐵 (𝐵𝑥) = ∅))
502, 49biimtrid 242 . . 3 ( E We 𝐵 → (𝐵 ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
511, 50syl6com 37 . 2 ( E We 𝐴 → (𝐵𝐴 → (𝐵 ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅)))
52513imp 1110 1 (( E We 𝐴𝐵𝐴𝐵 ≠ ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1536  wex 1775  wcel 2105  wne 2937  wral 3058  wrex 3067  cin 3961  wss 3962  c0 4338   E cep 5587   Fr wfr 5637   We wwe 5639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642
This theorem is referenced by:  tz7.5  6406  onnseq  8382  finminlem  36300
  Copyright terms: Public domain W3C validator