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

Theorem wefrc 5632
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 5625 . . 3 (𝐵𝐴 → ( E We 𝐴 → E We 𝐵))
2 n0 4311 . . . 4 (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦𝐵)
3 ineq2 4171 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐵𝑥) = (𝐵𝑦))
43eqeq1d 2739 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝐵𝑥) = ∅ ↔ (𝐵𝑦) = ∅))
54rspcev 3584 . . . . . . . . 9 ((𝑦𝐵 ∧ (𝐵𝑦) = ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
65ex 414 . . . . . . . 8 (𝑦𝐵 → ((𝐵𝑦) = ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
76adantl 483 . . . . . . 7 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) = ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
8 inss1 4193 . . . . . . . . . . 11 (𝐵𝑦) ⊆ 𝐵
9 wefr 5628 . . . . . . . . . . . . 13 ( E We 𝐵 → E Fr 𝐵)
10 vex 3452 . . . . . . . . . . . . . . 15 𝑦 ∈ V
1110inex2 5280 . . . . . . . . . . . . . 14 (𝐵𝑦) ∈ V
1211epfrc 5624 . . . . . . . . . . . . 13 (( E Fr 𝐵 ∧ (𝐵𝑦) ⊆ 𝐵 ∧ (𝐵𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)
139, 12syl3an1 1164 . . . . . . . . . . . 12 (( E We 𝐵 ∧ (𝐵𝑦) ⊆ 𝐵 ∧ (𝐵𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)
14133exp 1120 . . . . . . . . . . 11 ( E We 𝐵 → ((𝐵𝑦) ⊆ 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)))
158, 14mpi 20 . . . . . . . . . 10 ( E We 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅))
16 rexin 4204 . . . . . . . . . 10 (∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅ ↔ ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅))
1715, 16syl6ib 251 . . . . . . . . 9 ( E We 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
1817adantr 482 . . . . . . . 8 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
19 elin 3931 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐵𝑥) ↔ (𝑧𝐵𝑧𝑥))
20 df-3an 1090 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐵𝑧𝐵𝑥𝐵) ↔ ((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵))
21 3anrot 1101 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐵𝑧𝐵𝑥𝐵) ↔ (𝑧𝐵𝑥𝐵𝑦𝐵))
2220, 21bitr3i 277 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵) ↔ (𝑧𝐵𝑥𝐵𝑦𝐵))
23 wetrep 5631 . . . . . . . . . . . . . . . . . . . . . . 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 3150 . . . . . . . . . . . . 13 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → ∀𝑧 ∈ (𝐵𝑥)𝑧𝑦))
34 dfss3 3937 . . . . . . . . . . . . 13 ((𝐵𝑥) ⊆ 𝑦 ↔ ∀𝑧 ∈ (𝐵𝑥)𝑧𝑦)
3533, 34syl6ibr 252 . . . . . . . . . . . 12 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (𝐵𝑥) ⊆ 𝑦))
36 dfss 3933 . . . . . . . . . . . . . . 15 ((𝐵𝑥) ⊆ 𝑦 ↔ (𝐵𝑥) = ((𝐵𝑥) ∩ 𝑦))
37 in32 4186 . . . . . . . . . . . . . . . 16 ((𝐵𝑥) ∩ 𝑦) = ((𝐵𝑦) ∩ 𝑥)
3837eqeq2i 2750 . . . . . . . . . . . . . . 15 ((𝐵𝑥) = ((𝐵𝑥) ∩ 𝑦) ↔ (𝐵𝑥) = ((𝐵𝑦) ∩ 𝑥))
3936, 38sylbb 218 . . . . . . . . . . . . . 14 ((𝐵𝑥) ⊆ 𝑦 → (𝐵𝑥) = ((𝐵𝑦) ∩ 𝑥))
4039eqeq1d 2739 . . . . . . . . . . . . 13 ((𝐵𝑥) ⊆ 𝑦 → ((𝐵𝑥) = ∅ ↔ ((𝐵𝑦) ∩ 𝑥) = ∅))
4140biimprd 248 . . . . . . . . . . . 12 ((𝐵𝑥) ⊆ 𝑦 → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅))
4235, 41syl6 35 . . . . . . . . . . 11 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅)))
4342expd 417 . . . . . . . . . 10 (( E We 𝐵𝑦𝐵) → (𝑥𝐵 → (𝑥𝑦 → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅))))
4443imp4a 424 . . . . . . . . 9 (( E We 𝐵𝑦𝐵) → (𝑥𝐵 → ((𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) → (𝐵𝑥) = ∅)))
4544reximdvai 3163 . . . . . . . 8 (( E We 𝐵𝑦𝐵) → (∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅))
4618, 45syld 47 . . . . . . 7 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
477, 46pm2.61dne 3032 . . . . . 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 2944  wral 3065  wrex 3074  cin 3914  wss 3915  c0 4287   E cep 5541   Fr wfr 5590   We wwe 5592
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 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
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 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595
This theorem is referenced by:  tz7.5  6343  onnseq  8295  finminlem  34819
  Copyright terms: Public domain W3C validator