ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2dom GIF version

Theorem 2dom 6451
Description: A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.)
Assertion
Ref Expression
2dom (2𝑜𝐴 → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 = 𝑦)
Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem 2dom
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 df2o2 6127 . . . 4 2𝑜 = {∅, {∅}}
21breq1i 3818 . . 3 (2𝑜𝐴 ↔ {∅, {∅}} ≼ 𝐴)
3 brdomi 6395 . . 3 ({∅, {∅}} ≼ 𝐴 → ∃𝑓 𝑓:{∅, {∅}}–1-1𝐴)
42, 3sylbi 119 . 2 (2𝑜𝐴 → ∃𝑓 𝑓:{∅, {∅}}–1-1𝐴)
5 f1f 5163 . . . . 5 (𝑓:{∅, {∅}}–1-1𝐴𝑓:{∅, {∅}}⟶𝐴)
6 0ex 3931 . . . . . 6 ∅ ∈ V
76prid1 3522 . . . . 5 ∅ ∈ {∅, {∅}}
8 ffvelrn 5376 . . . . 5 ((𝑓:{∅, {∅}}⟶𝐴 ∧ ∅ ∈ {∅, {∅}}) → (𝑓‘∅) ∈ 𝐴)
95, 7, 8sylancl 404 . . . 4 (𝑓:{∅, {∅}}–1-1𝐴 → (𝑓‘∅) ∈ 𝐴)
10 p0ex 3986 . . . . . 6 {∅} ∈ V
1110prid2 3523 . . . . 5 {∅} ∈ {∅, {∅}}
12 ffvelrn 5376 . . . . 5 ((𝑓:{∅, {∅}}⟶𝐴 ∧ {∅} ∈ {∅, {∅}}) → (𝑓‘{∅}) ∈ 𝐴)
135, 11, 12sylancl 404 . . . 4 (𝑓:{∅, {∅}}–1-1𝐴 → (𝑓‘{∅}) ∈ 𝐴)
14 0nep0 3965 . . . . . 6 ∅ ≠ {∅}
1514neii 2251 . . . . 5 ¬ ∅ = {∅}
16 f1fveq 5490 . . . . . 6 ((𝑓:{∅, {∅}}–1-1𝐴 ∧ (∅ ∈ {∅, {∅}} ∧ {∅} ∈ {∅, {∅}})) → ((𝑓‘∅) = (𝑓‘{∅}) ↔ ∅ = {∅}))
177, 11, 16mpanr12 430 . . . . 5 (𝑓:{∅, {∅}}–1-1𝐴 → ((𝑓‘∅) = (𝑓‘{∅}) ↔ ∅ = {∅}))
1815, 17mtbiri 633 . . . 4 (𝑓:{∅, {∅}}–1-1𝐴 → ¬ (𝑓‘∅) = (𝑓‘{∅}))
19 eqeq1 2089 . . . . . 6 (𝑥 = (𝑓‘∅) → (𝑥 = 𝑦 ↔ (𝑓‘∅) = 𝑦))
2019notbid 625 . . . . 5 (𝑥 = (𝑓‘∅) → (¬ 𝑥 = 𝑦 ↔ ¬ (𝑓‘∅) = 𝑦))
21 eqeq2 2092 . . . . . 6 (𝑦 = (𝑓‘{∅}) → ((𝑓‘∅) = 𝑦 ↔ (𝑓‘∅) = (𝑓‘{∅})))
2221notbid 625 . . . . 5 (𝑦 = (𝑓‘{∅}) → (¬ (𝑓‘∅) = 𝑦 ↔ ¬ (𝑓‘∅) = (𝑓‘{∅})))
2320, 22rspc2ev 2725 . . . 4 (((𝑓‘∅) ∈ 𝐴 ∧ (𝑓‘{∅}) ∈ 𝐴 ∧ ¬ (𝑓‘∅) = (𝑓‘{∅})) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 = 𝑦)
249, 13, 18, 23syl3anc 1170 . . 3 (𝑓:{∅, {∅}}–1-1𝐴 → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 = 𝑦)
2524exlimiv 1530 . 2 (∃𝑓 𝑓:{∅, {∅}}–1-1𝐴 → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 = 𝑦)
264, 25syl 14 1 (2𝑜𝐴 → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 = 𝑦)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 103   = wceq 1285  wex 1422  wcel 1434  wrex 2354  c0 3269  {csn 3422  {cpr 3423   class class class wbr 3811  wf 4964  1-1wf1 4965  cfv 4968  2𝑜c2o 6106  cdom 6385
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-nul 3930  ax-pow 3974  ax-pr 3999  ax-un 4223
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-v 2614  df-sbc 2827  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-opab 3866  df-id 4083  df-suc 4161  df-xp 4406  df-rel 4407  df-cnv 4408  df-co 4409  df-dm 4410  df-rn 4411  df-iota 4933  df-fun 4970  df-fn 4971  df-f 4972  df-f1 4973  df-fv 4976  df-1o 6112  df-2o 6113  df-dom 6388
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator