HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem 2dom 4408
Description: A set that dominates ordinal 2 has at least 2 different members.
Hypothesis
Ref Expression
2dom.1 |- A e. V
Assertion
Ref Expression
2dom |- (2o ~<_ A -> E.x e. A E.y e. A -. x = y)
Distinct variable group:   x,y,A
Proof of Theorem 2dom
StepHypRef Expression
1 df2o2 4125 . . . 4 |- 2o = {(/), {(/)}}
21breq1i 2616 . . 3 |- (2o ~<_ A <-> {(/), {(/)}} ~<_ A)
3 2dom.1 . . . 4 |- A e. V
43brdom 4360 . . 3 |- ({(/), {(/)}} ~<_ A <-> E.f f:{(/), {(/)}}-1-1->A)
52, 4bitr 173 . 2 |- (2o ~<_ A <-> E.f f:{(/), {(/)}}-1-1->A)
6 eqeq1 1473 . . . . . 6 |- (x = (f` (/)) -> (x = y <-> (f` (/)) = y))
76negbid 609 . . . . 5 |- (x = (f` (/)) -> (-. x = y <-> -. (f` (/)) = y))
8 eqeq2 1476 . . . . . 6 |- (y = (f` {(/)}) -> ((f` (/)) = y <-> (f` (/)) = (f` {(/)})))
98negbid 609 . . . . 5 |- (y = (f` {(/)}) -> (-. (f` (/)) = y <-> -. (f` (/)) = (f` {(/)})))
107, 9rcla42ev 1872 . . . 4 |- (((f` (/)) e. A /\ (f` {(/)}) e. A /\ -. (f` (/)) = (f` {(/)})) -> E.x e. A E.y e. A -. x = y)
11 f1f 3650 . . . . 5 |- (f:{(/), {(/)}}-1-1->A -> f:{(/), {(/)}}-->A)
12 0ex 2701 . . . . . . 7 |- (/) e. V
1312pri1 2441 . . . . . 6 |- (/) e. {(/), {(/)}}
14 ffvelrn 3799 . . . . . 6 |- ((f:{(/), {(/)}}-->A /\ (/) e. {(/), {(/)}}) -> (f` (/)) e. A)
1513, 14mpan2 694 . . . . 5 |- (f:{(/), {(/)}}-->A -> (f` (/)) e. A)
1611, 15syl 10 . . . 4 |- (f:{(/), {(/)}}-1-1->A -> (f` (/)) e. A)
17 p0ex 2760 . . . . . . 7 |- {(/)} e. V
1817pri2 2442 . . . . . 6 |- {(/)} e. {(/), {(/)}}
19 ffvelrn 3799 . . . . . 6 |- ((f:{(/), {(/)}}-->A /\ {(/)} e. {(/), {(/)}}) -> (f` {(/)}) e. A)
2018, 19mpan2 694 . . . . 5 |- (f:{(/), {(/)}}-->A -> (f` {(/)}) e. A)
2111, 20syl 10 . . . 4 |- (f:{(/), {(/)}}-1-1->A -> (f` {(/)}) e. A)
22 0nep0 2727 . . . . . 6 |- (/) =/= {(/)}
23 df-ne 1579 . . . . . 6 |- ((/) =/= {(/)} <-> -. (/) = {(/)})
2422, 23mpbi 189 . . . . 5 |- -. (/) = {(/)}
2513, 18pm3.2i 285 . . . . . 6 |- ((/) e. {(/), {(/)}} /\ {(/)} e. {(/), {(/)}})
26 f1fveq 3861 . . . . . 6 |- ((f:{(/), {(/)}}-1-1->A /\ ((/) e. {(/), {(/)}} /\ {(/)} e. {(/), {(/)}})) -> ((f` (/)) = (f` {(/)}) <-> (/) = {(/)}))
2725, 26mpan2 694 . . . . 5 |- (f:{(/), {(/)}}-1-1->A -> ((f` (/)) = (f` {(/)}) <-> (/) = {(/)}))
2824, 27mtbiri 715 . . . 4 |- (f:{(/), {(/)}}-1-1->A -> -. (f` (/)) = (f` {(/)}))
2910, 16, 21, 28syl3anc 856 . . 3 |- (f:{(/), {(/)}}-1-1->A -> E.x e. A E.y e. A -. x = y)
302919.23aiv 1290 . 2 |- (E.f f:{(/), {(/)}}-1-1->A -> E.x e. A E.y e. A -. x = y)
315, 30sylbi 199 1 |- (2o ~<_ A -> E.x e. A E.y e. A -. x = y)
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977   =/= wne 1577  E.wrex 1638  Vcvv 1802  (/)c0 2270  {csn 2399  {cpr 2400   class class class wbr 2609  -->wf 3168  -1-1->wf1 3169  ` cfv 3172  2oc2o 4113   ~<_ cdom 4349
This theorem is referenced by:  unxpdomlem 4815
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-id 2824  df-suc 2944  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-f1 3185  df-fv 3188  df-1o 4117  df-2o 4118  df-dom 4352
Copyright terms: Public domain