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

Theorem wefrc 5671
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 5664 . . 3 (𝐵𝐴 → ( E We 𝐴 → E We 𝐵))
2 n0 4347 . . . 4 (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦𝐵)
3 ineq2 4207 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐵𝑥) = (𝐵𝑦))
43eqeq1d 2735 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝐵𝑥) = ∅ ↔ (𝐵𝑦) = ∅))
54rspcev 3613 . . . . . . . . 9 ((𝑦𝐵 ∧ (𝐵𝑦) = ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
65ex 414 . . . . . . . 8 (𝑦𝐵 → ((𝐵𝑦) = ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
76adantl 483 . . . . . . 7 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) = ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
8 inss1 4229 . . . . . . . . . . 11 (𝐵𝑦) ⊆ 𝐵
9 wefr 5667 . . . . . . . . . . . . 13 ( E We 𝐵 → E Fr 𝐵)
10 vex 3479 . . . . . . . . . . . . . . 15 𝑦 ∈ V
1110inex2 5319 . . . . . . . . . . . . . 14 (𝐵𝑦) ∈ V
1211epfrc 5663 . . . . . . . . . . . . 13 (( E Fr 𝐵 ∧ (𝐵𝑦) ⊆ 𝐵 ∧ (𝐵𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)
139, 12syl3an1 1164 . . . . . . . . . . . 12 (( E We 𝐵 ∧ (𝐵𝑦) ⊆ 𝐵 ∧ (𝐵𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)
14133exp 1120 . . . . . . . . . . 11 ( E We 𝐵 → ((𝐵𝑦) ⊆ 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)))
158, 14mpi 20 . . . . . . . . . 10 ( E We 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅))
16 rexin 4240 . . . . . . . . . 10 (∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅ ↔ ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅))
1715, 16imbitrdi 250 . . . . . . . . 9 ( E We 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
1817adantr 482 . . . . . . . 8 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
19 elin 3965 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐵𝑥) ↔ (𝑧𝐵𝑧𝑥))
20 df-3an 1090 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐵𝑧𝐵𝑥𝐵) ↔ ((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵))
21 3anrot 1101 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐵𝑧𝐵𝑥𝐵) ↔ (𝑧𝐵𝑥𝐵𝑦𝐵))
2220, 21bitr3i 277 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵) ↔ (𝑧𝐵𝑥𝐵𝑦𝐵))
23 wetrep 5670 . . . . . . . . . . . . . . . . . . . . . . 23 (( E We 𝐵 ∧ (𝑧𝐵𝑥𝐵𝑦𝐵)) → ((𝑧𝑥𝑥𝑦) → 𝑧𝑦))
2423expd 417 . . . . . . . . . . . . . . . . . . . . . 22 (( E We 𝐵 ∧ (𝑧𝐵𝑥𝐵𝑦𝐵)) → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))
2522, 24sylan2b 595 . . . . . . . . . . . . . . . . . . . . 21 (( E We 𝐵 ∧ ((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵)) → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))
2625exp44 439 . . . . . . . . . . . . . . . . . . . 20 ( E We 𝐵 → (𝑦𝐵 → (𝑧𝐵 → (𝑥𝐵 → (𝑧𝑥 → (𝑥𝑦𝑧𝑦))))))
2726imp 408 . . . . . . . . . . . . . . . . . . 19 (( E We 𝐵𝑦𝐵) → (𝑧𝐵 → (𝑥𝐵 → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))))
2827com34 91 . . . . . . . . . . . . . . . . . 18 (( E We 𝐵𝑦𝐵) → (𝑧𝐵 → (𝑧𝑥 → (𝑥𝐵 → (𝑥𝑦𝑧𝑦)))))
2928impd 412 . . . . . . . . . . . . . . . . 17 (( E We 𝐵𝑦𝐵) → ((𝑧𝐵𝑧𝑥) → (𝑥𝐵 → (𝑥𝑦𝑧𝑦))))
3019, 29biimtrid 241 . . . . . . . . . . . . . . . 16 (( E We 𝐵𝑦𝐵) → (𝑧 ∈ (𝐵𝑥) → (𝑥𝐵 → (𝑥𝑦𝑧𝑦))))
3130imp4a 424 . . . . . . . . . . . . . . 15 (( E We 𝐵𝑦𝐵) → (𝑧 ∈ (𝐵𝑥) → ((𝑥𝐵𝑥𝑦) → 𝑧𝑦)))
3231com23 86 . . . . . . . . . . . . . 14 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (𝑧 ∈ (𝐵𝑥) → 𝑧𝑦)))
3332ralrimdv 3153 . . . . . . . . . . . . 13 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → ∀𝑧 ∈ (𝐵𝑥)𝑧𝑦))
34 dfss3 3971 . . . . . . . . . . . . 13 ((𝐵𝑥) ⊆ 𝑦 ↔ ∀𝑧 ∈ (𝐵𝑥)𝑧𝑦)
3533, 34imbitrrdi 251 . . . . . . . . . . . 12 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (𝐵𝑥) ⊆ 𝑦))
36 dfss 3967 . . . . . . . . . . . . . . 15 ((𝐵𝑥) ⊆ 𝑦 ↔ (𝐵𝑥) = ((𝐵𝑥) ∩ 𝑦))
37 in32 4222 . . . . . . . . . . . . . . . 16 ((𝐵𝑥) ∩ 𝑦) = ((𝐵𝑦) ∩ 𝑥)
3837eqeq2i 2746 . . . . . . . . . . . . . . 15 ((𝐵𝑥) = ((𝐵𝑥) ∩ 𝑦) ↔ (𝐵𝑥) = ((𝐵𝑦) ∩ 𝑥))
3936, 38sylbb 218 . . . . . . . . . . . . . 14 ((𝐵𝑥) ⊆ 𝑦 → (𝐵𝑥) = ((𝐵𝑦) ∩ 𝑥))
4039eqeq1d 2735 . . . . . . . . . . . . 13 ((𝐵𝑥) ⊆ 𝑦 → ((𝐵𝑥) = ∅ ↔ ((𝐵𝑦) ∩ 𝑥) = ∅))
4140biimprd 247 . . . . . . . . . . . 12 ((𝐵𝑥) ⊆ 𝑦 → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅))
4235, 41syl6 35 . . . . . . . . . . 11 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅)))
4342expd 417 . . . . . . . . . 10 (( E We 𝐵𝑦𝐵) → (𝑥𝐵 → (𝑥𝑦 → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅))))
4443imp4a 424 . . . . . . . . 9 (( E We 𝐵𝑦𝐵) → (𝑥𝐵 → ((𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) → (𝐵𝑥) = ∅)))
4544reximdvai 3166 . . . . . . . 8 (( E We 𝐵𝑦𝐵) → (∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅))
4618, 45syld 47 . . . . . . 7 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
477, 46pm2.61dne 3029 . . . . . 6 (( E We 𝐵𝑦𝐵) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
4847ex 414 . . . . 5 ( E We 𝐵 → (𝑦𝐵 → ∃𝑥𝐵 (𝐵𝑥) = ∅))
4948exlimdv 1937 . . . 4 ( E We 𝐵 → (∃𝑦 𝑦𝐵 → ∃𝑥𝐵 (𝐵𝑥) = ∅))
502, 49biimtrid 241 . . 3 ( E We 𝐵 → (𝐵 ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
511, 50syl6com 37 . 2 ( E We 𝐴 → (𝐵𝐴 → (𝐵 ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅)))
52513imp 1112 1 (( E We 𝐴𝐵𝐴𝐵 ≠ ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088   = wceq 1542  wex 1782  wcel 2107  wne 2941  wral 3062  wrex 3071  cin 3948  wss 3949  c0 4323   E cep 5580   Fr wfr 5629   We wwe 5631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634
This theorem is referenced by:  tz7.5  6386  onnseq  8344  finminlem  35203
  Copyright terms: Public domain W3C validator