MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  npomex Structured version   Unicode version

Theorem npomex 9186
Description: A simplifying observation, and an indication of why any attempt to develop a theory of the real numbers without the Axiom of Infinity is doomed to failure: since every member of  P. is an infinite set, the negation of Infinity implies that  P., and hence 
RR, is empty. (Note that this proof, which used the fact that Dedekind cuts have no maximum, could just as well have used that they have no minimum, since they are downward-closed by prcdnq 9183 and nsmallnq 9167). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.)
Assertion
Ref Expression
npomex  |-  ( A  e.  P.  ->  om  e.  _V )

Proof of Theorem npomex
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3002 . . . 4  |-  ( A  e.  P.  ->  A  e.  _V )
2 prnmax 9185 . . . . . 6  |-  ( ( A  e.  P.  /\  x  e.  A )  ->  E. y  e.  A  x  <Q  y )
32ralrimiva 2820 . . . . 5  |-  ( A  e.  P.  ->  A. x  e.  A  E. y  e.  A  x  <Q  y )
4 prpssnq 9180 . . . . . . . . . . 11  |-  ( A  e.  P.  ->  A  C. 
Q. )
54pssssd 3474 . . . . . . . . . 10  |-  ( A  e.  P.  ->  A  C_ 
Q. )
6 ltsonq 9159 . . . . . . . . . 10  |-  <Q  Or  Q.
7 soss 4680 . . . . . . . . . 10  |-  ( A 
C_  Q.  ->  (  <Q  Or  Q.  ->  <Q  Or  A
) )
85, 6, 7mpisyl 18 . . . . . . . . 9  |-  ( A  e.  P.  ->  <Q  Or  A )
98adantr 465 . . . . . . . 8  |-  ( ( A  e.  P.  /\  A  e.  Fin )  ->  <Q  Or  A )
10 simpr 461 . . . . . . . 8  |-  ( ( A  e.  P.  /\  A  e.  Fin )  ->  A  e.  Fin )
11 prn0 9179 . . . . . . . . 9  |-  ( A  e.  P.  ->  A  =/=  (/) )
1211adantr 465 . . . . . . . 8  |-  ( ( A  e.  P.  /\  A  e.  Fin )  ->  A  =/=  (/) )
13 fimax2g 7579 . . . . . . . 8  |-  ( ( 
<Q  Or  A  /\  A  e.  Fin  /\  A  =/=  (/) )  ->  E. x  e.  A  A. y  e.  A  -.  x  <Q  y )
149, 10, 12, 13syl3anc 1218 . . . . . . 7  |-  ( ( A  e.  P.  /\  A  e.  Fin )  ->  E. x  e.  A  A. y  e.  A  -.  x  <Q  y )
15 ralnex 2746 . . . . . . . . 9  |-  ( A. y  e.  A  -.  x  <Q  y  <->  -.  E. y  e.  A  x  <Q  y )
1615rexbii 2761 . . . . . . . 8  |-  ( E. x  e.  A  A. y  e.  A  -.  x  <Q  y  <->  E. x  e.  A  -.  E. y  e.  A  x  <Q  y )
17 rexnal 2747 . . . . . . . 8  |-  ( E. x  e.  A  -.  E. y  e.  A  x 
<Q  y  <->  -.  A. x  e.  A  E. y  e.  A  x  <Q  y )
1816, 17bitri 249 . . . . . . 7  |-  ( E. x  e.  A  A. y  e.  A  -.  x  <Q  y  <->  -.  A. x  e.  A  E. y  e.  A  x  <Q  y )
1914, 18sylib 196 . . . . . 6  |-  ( ( A  e.  P.  /\  A  e.  Fin )  ->  -.  A. x  e.  A  E. y  e.  A  x  <Q  y
)
2019ex 434 . . . . 5  |-  ( A  e.  P.  ->  ( A  e.  Fin  ->  -.  A. x  e.  A  E. y  e.  A  x  <Q  y ) )
213, 20mt2d 117 . . . 4  |-  ( A  e.  P.  ->  -.  A  e.  Fin )
22 nelne1 2722 . . . 4  |-  ( ( A  e.  _V  /\  -.  A  e.  Fin )  ->  _V  =/=  Fin )
231, 21, 22syl2anc 661 . . 3  |-  ( A  e.  P.  ->  _V  =/=  Fin )
2423necomd 2640 . 2  |-  ( A  e.  P.  ->  Fin  =/=  _V )
25 fineqv 7549 . . 3  |-  ( -. 
om  e.  _V  <->  Fin  =  _V )
2625necon1abii 2686 . 2  |-  ( Fin 
=/=  _V  <->  om  e.  _V )
2724, 26sylib 196 1  |-  ( A  e.  P.  ->  om  e.  _V )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    e. wcel 1756    =/= wne 2620   A.wral 2736   E.wrex 2737   _Vcvv 2993    C_ wss 3349   (/)c0 3658   class class class wbr 4313    Or wor 4661   omcom 6497   Fincfn 7331   Q.cnq 9040    <Q cltq 9046   P.cnp 9047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-om 6498  df-1st 6598  df-2nd 6599  df-recs 6853  df-rdg 6887  df-1o 6941  df-oadd 6945  df-omul 6946  df-er 7122  df-en 7332  df-dom 7333  df-sdom 7334  df-fin 7335  df-ni 9062  df-mi 9064  df-lti 9065  df-ltpq 9100  df-enq 9101  df-nq 9102  df-ltnq 9108  df-np 9171
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator