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 ( 𝐴P → ω ∈ V )

Proof

Step Hyp Ref Expression
1 elex ( 𝐴P𝐴 ∈ V )
2 prnmax ( ( 𝐴P𝑥𝐴 ) → ∃ 𝑦𝐴 𝑥 <Q 𝑦 )
3 2 ralrimiva ( 𝐴P → ∀ 𝑥𝐴𝑦𝐴 𝑥 <Q 𝑦 )
4 prpssnq ( 𝐴P𝐴Q )
5 4 pssssd ( 𝐴P𝐴Q )
6 ltsonq <Q Or Q
7 soss ( 𝐴Q → ( <Q Or Q → <Q Or 𝐴 ) )
8 5 6 7 mpisyl ( 𝐴P → <Q Or 𝐴 )
9 8 adantr ( ( 𝐴P𝐴 ∈ Fin ) → <Q Or 𝐴 )
10 simpr ( ( 𝐴P𝐴 ∈ Fin ) → 𝐴 ∈ Fin )
11 prn0 ( 𝐴P𝐴 ≠ ∅ )
12 11 adantr ( ( 𝐴P𝐴 ∈ Fin ) → 𝐴 ≠ ∅ )
13 fimax2g ( ( <Q Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <Q 𝑦 )
14 9 10 12 13 syl3anc ( ( 𝐴P𝐴 ∈ Fin ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <Q 𝑦 )
15 ralnex ( ∀ 𝑦𝐴 ¬ 𝑥 <Q 𝑦 ↔ ¬ ∃ 𝑦𝐴 𝑥 <Q 𝑦 )
16 15 rexbii ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <Q 𝑦 ↔ ∃ 𝑥𝐴 ¬ ∃ 𝑦𝐴 𝑥 <Q 𝑦 )
17 rexnal ( ∃ 𝑥𝐴 ¬ ∃ 𝑦𝐴 𝑥 <Q 𝑦 ↔ ¬ ∀ 𝑥𝐴𝑦𝐴 𝑥 <Q 𝑦 )
18 16 17 bitri ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <Q 𝑦 ↔ ¬ ∀ 𝑥𝐴𝑦𝐴 𝑥 <Q 𝑦 )
19 14 18 sylib ( ( 𝐴P𝐴 ∈ Fin ) → ¬ ∀ 𝑥𝐴𝑦𝐴 𝑥 <Q 𝑦 )
20 19 ex ( 𝐴P → ( 𝐴 ∈ Fin → ¬ ∀ 𝑥𝐴𝑦𝐴 𝑥 <Q 𝑦 ) )
21 3 20 mt2d ( 𝐴P → ¬ 𝐴 ∈ Fin )
22 nelne1 ( ( 𝐴 ∈ V ∧ ¬ 𝐴 ∈ Fin ) → V ≠ Fin )
23 1 21 22 syl2anc ( 𝐴P → V ≠ Fin )
24 23 necomd ( 𝐴P → Fin ≠ V )
25 fineqv ( ¬ ω ∈ V ↔ Fin = V )
26 25 necon1abii ( Fin ≠ V ↔ ω ∈ V )
27 24 26 sylib ( 𝐴P → ω ∈ V )