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

Theorem wefrc 5303
Description: A nonempty (possibly proper) subclass of a class well-ordered by E 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 5296 . . 3 (𝐵𝐴 → ( E We 𝐴 → E We 𝐵))
2 n0 4130 . . . 4 (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦𝐵)
3 ineq2 4005 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐵𝑥) = (𝐵𝑦))
43eqeq1d 2806 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝐵𝑥) = ∅ ↔ (𝐵𝑦) = ∅))
54rspcev 3500 . . . . . . . . 9 ((𝑦𝐵 ∧ (𝐵𝑦) = ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
65ex 399 . . . . . . . 8 (𝑦𝐵 → ((𝐵𝑦) = ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
76adantl 469 . . . . . . 7 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) = ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
8 inss1 4027 . . . . . . . . . . 11 (𝐵𝑦) ⊆ 𝐵
9 wefr 5299 . . . . . . . . . . . . 13 ( E We 𝐵 → E Fr 𝐵)
10 vex 3392 . . . . . . . . . . . . . . 15 𝑦 ∈ V
1110inex2 4993 . . . . . . . . . . . . . 14 (𝐵𝑦) ∈ V
1211epfrc 5295 . . . . . . . . . . . . 13 (( E Fr 𝐵 ∧ (𝐵𝑦) ⊆ 𝐵 ∧ (𝐵𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)
139, 12syl3an1 1195 . . . . . . . . . . . 12 (( E We 𝐵 ∧ (𝐵𝑦) ⊆ 𝐵 ∧ (𝐵𝑦) ≠ ∅) → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)
14133exp 1141 . . . . . . . . . . 11 ( E We 𝐵 → ((𝐵𝑦) ⊆ 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅)))
158, 14mpi 20 . . . . . . . . . 10 ( E We 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅))
16 elin 3993 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐵𝑦) ↔ (𝑥𝐵𝑥𝑦))
1716anbi1i 612 . . . . . . . . . . . 12 ((𝑥 ∈ (𝐵𝑦) ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) ↔ ((𝑥𝐵𝑥𝑦) ∧ ((𝐵𝑦) ∩ 𝑥) = ∅))
18 anass 456 . . . . . . . . . . . 12 (((𝑥𝐵𝑥𝑦) ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) ↔ (𝑥𝐵 ∧ (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
1917, 18bitri 266 . . . . . . . . . . 11 ((𝑥 ∈ (𝐵𝑦) ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) ↔ (𝑥𝐵 ∧ (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
2019rexbii2 3225 . . . . . . . . . 10 (∃𝑥 ∈ (𝐵𝑦)((𝐵𝑦) ∩ 𝑥) = ∅ ↔ ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅))
2115, 20syl6ib 242 . . . . . . . . 9 ( E We 𝐵 → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
2221adantr 468 . . . . . . . 8 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅)))
23 elin 3993 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐵𝑥) ↔ (𝑧𝐵𝑧𝑥))
24 df-3an 1102 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐵𝑧𝐵𝑥𝐵) ↔ ((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵))
25 3anrot 1115 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐵𝑧𝐵𝑥𝐵) ↔ (𝑧𝐵𝑥𝐵𝑦𝐵))
2624, 25bitr3i 268 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵) ↔ (𝑧𝐵𝑥𝐵𝑦𝐵))
27 wetrep 5302 . . . . . . . . . . . . . . . . . . . . . . 23 (( E We 𝐵 ∧ (𝑧𝐵𝑥𝐵𝑦𝐵)) → ((𝑧𝑥𝑥𝑦) → 𝑧𝑦))
2827expd 402 . . . . . . . . . . . . . . . . . . . . . 22 (( E We 𝐵 ∧ (𝑧𝐵𝑥𝐵𝑦𝐵)) → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))
2926, 28sylan2b 583 . . . . . . . . . . . . . . . . . . . . 21 (( E We 𝐵 ∧ ((𝑦𝐵𝑧𝐵) ∧ 𝑥𝐵)) → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))
3029exp44 426 . . . . . . . . . . . . . . . . . . . 20 ( E We 𝐵 → (𝑦𝐵 → (𝑧𝐵 → (𝑥𝐵 → (𝑧𝑥 → (𝑥𝑦𝑧𝑦))))))
3130imp 395 . . . . . . . . . . . . . . . . . . 19 (( E We 𝐵𝑦𝐵) → (𝑧𝐵 → (𝑥𝐵 → (𝑧𝑥 → (𝑥𝑦𝑧𝑦)))))
3231com34 91 . . . . . . . . . . . . . . . . . 18 (( E We 𝐵𝑦𝐵) → (𝑧𝐵 → (𝑧𝑥 → (𝑥𝐵 → (𝑥𝑦𝑧𝑦)))))
3332impd 398 . . . . . . . . . . . . . . . . 17 (( E We 𝐵𝑦𝐵) → ((𝑧𝐵𝑧𝑥) → (𝑥𝐵 → (𝑥𝑦𝑧𝑦))))
3423, 33syl5bi 233 . . . . . . . . . . . . . . . 16 (( E We 𝐵𝑦𝐵) → (𝑧 ∈ (𝐵𝑥) → (𝑥𝐵 → (𝑥𝑦𝑧𝑦))))
3534imp4a 411 . . . . . . . . . . . . . . 15 (( E We 𝐵𝑦𝐵) → (𝑧 ∈ (𝐵𝑥) → ((𝑥𝐵𝑥𝑦) → 𝑧𝑦)))
3635com23 86 . . . . . . . . . . . . . 14 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (𝑧 ∈ (𝐵𝑥) → 𝑧𝑦)))
3736ralrimdv 3154 . . . . . . . . . . . . 13 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → ∀𝑧 ∈ (𝐵𝑥)𝑧𝑦))
38 dfss3 3785 . . . . . . . . . . . . 13 ((𝐵𝑥) ⊆ 𝑦 ↔ ∀𝑧 ∈ (𝐵𝑥)𝑧𝑦)
3937, 38syl6ibr 243 . . . . . . . . . . . 12 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (𝐵𝑥) ⊆ 𝑦))
40 dfss 3782 . . . . . . . . . . . . . . 15 ((𝐵𝑥) ⊆ 𝑦 ↔ (𝐵𝑥) = ((𝐵𝑥) ∩ 𝑦))
41 in32 4020 . . . . . . . . . . . . . . . 16 ((𝐵𝑥) ∩ 𝑦) = ((𝐵𝑦) ∩ 𝑥)
4241eqeq2i 2816 . . . . . . . . . . . . . . 15 ((𝐵𝑥) = ((𝐵𝑥) ∩ 𝑦) ↔ (𝐵𝑥) = ((𝐵𝑦) ∩ 𝑥))
4340, 42sylbb 210 . . . . . . . . . . . . . 14 ((𝐵𝑥) ⊆ 𝑦 → (𝐵𝑥) = ((𝐵𝑦) ∩ 𝑥))
4443eqeq1d 2806 . . . . . . . . . . . . 13 ((𝐵𝑥) ⊆ 𝑦 → ((𝐵𝑥) = ∅ ↔ ((𝐵𝑦) ∩ 𝑥) = ∅))
4544biimprd 239 . . . . . . . . . . . 12 ((𝐵𝑥) ⊆ 𝑦 → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅))
4639, 45syl6 35 . . . . . . . . . . 11 (( E We 𝐵𝑦𝐵) → ((𝑥𝐵𝑥𝑦) → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅)))
4746expd 402 . . . . . . . . . 10 (( E We 𝐵𝑦𝐵) → (𝑥𝐵 → (𝑥𝑦 → (((𝐵𝑦) ∩ 𝑥) = ∅ → (𝐵𝑥) = ∅))))
4847imp4a 411 . . . . . . . . 9 (( E We 𝐵𝑦𝐵) → (𝑥𝐵 → ((𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) → (𝐵𝑥) = ∅)))
4948reximdvai 3200 . . . . . . . 8 (( E We 𝐵𝑦𝐵) → (∃𝑥𝐵 (𝑥𝑦 ∧ ((𝐵𝑦) ∩ 𝑥) = ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅))
5022, 49syld 47 . . . . . . 7 (( E We 𝐵𝑦𝐵) → ((𝐵𝑦) ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
517, 50pm2.61dne 3062 . . . . . 6 (( E We 𝐵𝑦𝐵) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
5251ex 399 . . . . 5 ( E We 𝐵 → (𝑦𝐵 → ∃𝑥𝐵 (𝐵𝑥) = ∅))
5352exlimdv 2024 . . . 4 ( E We 𝐵 → (∃𝑦 𝑦𝐵 → ∃𝑥𝐵 (𝐵𝑥) = ∅))
542, 53syl5bi 233 . . 3 ( E We 𝐵 → (𝐵 ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅))
551, 54syl6com 37 . 2 ( E We 𝐴 → (𝐵𝐴 → (𝐵 ≠ ∅ → ∃𝑥𝐵 (𝐵𝑥) = ∅)))
56553imp 1130 1 (( E We 𝐴𝐵𝐴𝐵 ≠ ∅) → ∃𝑥𝐵 (𝐵𝑥) = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2156  wne 2976  wral 3094  wrex 3095  cin 3766  wss 3767  c0 4114   E cep 5221   Fr wfr 5265   We wwe 5267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-sep 4973  ax-nul 4981  ax-pr 5094
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ne 2977  df-ral 3099  df-rex 3100  df-rab 3103  df-v 3391  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4115  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-br 4843  df-opab 4905  df-eprel 5222  df-po 5230  df-so 5231  df-fr 5268  df-we 5270
This theorem is referenced by:  tz7.5  5955  onnseq  7675  finminlem  32631
  Copyright terms: Public domain W3C validator