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 ( 𝐴 ∈ 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 )