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 )