This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem npomex

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 and nsmallnq ). (Contributed by Mario Carneiro, 11-May-2013) (Revised by Mario Carneiro, 16-Nov-2014) (New usage is discouraged.)

Ref Expression
Assertion npomex 
|- ( A e. P. -> _om e. _V )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. P. -> A e. _V )
2 prnmax 
 |-  ( ( A e. P. /\ x e. A ) -> E. y e. A x
3 2 ralrimiva 
 |-  ( A e. P. -> A. x e. A E. y e. A x
4 prpssnq 
 |-  ( A e. P. -> A C. Q. )
5 4 pssssd 
 |-  ( A e. P. -> A C_ Q. )
6 ltsonq 
 |-
7 soss 
 |-  ( A C_ Q. -> (
8 5 6 7 mpisyl 
 |-  ( A e. P. ->
9 8 adantr 
 |-  ( ( A e. P. /\ A e. Fin ) ->
10 simpr 
 |-  ( ( A e. P. /\ A e. Fin ) -> A e. Fin )
11 prn0 
 |-  ( A e. P. -> A =/= (/) )
12 11 adantr 
 |-  ( ( A e. P. /\ A e. Fin ) -> A =/= (/) )
13 fimax2g 
 |-  ( (  E. x e. A A. y e. A -. x
14 9 10 12 13 syl3anc 
 |-  ( ( A e. P. /\ A e. Fin ) -> E. x e. A A. y e. A -. x
15 ralnex 
 |-  ( A. y e. A -. x  -. E. y e. A x
16 15 rexbii 
 |-  ( E. x e. A A. y e. A -. x  E. x e. A -. E. y e. A x
17 rexnal 
 |-  ( E. x e. A -. E. y e. A x  -. A. x e. A E. y e. A x
18 16 17 bitri 
 |-  ( E. x e. A A. y e. A -. x  -. A. x e. A E. y e. A x
19 14 18 sylib 
 |-  ( ( A e. P. /\ A e. Fin ) -> -. A. x e. A E. y e. A x
20 19 ex 
 |-  ( A e. P. -> ( A e. Fin -> -. A. x e. A E. y e. A x
21 3 20 mt2d 
 |-  ( A e. P. -> -. A e. Fin )
22 nelne1 
 |-  ( ( A e. _V /\ -. A e. Fin ) -> _V =/= Fin )
23 1 21 22 syl2anc 
 |-  ( A e. P. -> _V =/= Fin )
24 23 necomd 
 |-  ( A e. P. -> Fin =/= _V )
25 fineqv 
 |-  ( -. _om e. _V <-> Fin = _V )
26 25 necon1abii 
 |-  ( Fin =/= _V <-> _om e. _V )
27 24 26 sylib 
 |-  ( A e. P. -> _om e. _V )