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

Theorem npomex 9697
 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 ℝ, 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 9694 and nsmallnq 9678). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.)
Assertion
Ref Expression
npomex (𝐴P → ω ∈ V)

Proof of Theorem npomex
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3185 . . . 4 (𝐴P𝐴 ∈ V)
2 prnmax 9696 . . . . . 6 ((𝐴P𝑥𝐴) → ∃𝑦𝐴 𝑥 <Q 𝑦)
32ralrimiva 2949 . . . . 5 (𝐴P → ∀𝑥𝐴𝑦𝐴 𝑥 <Q 𝑦)
4 prpssnq 9691 . . . . . . . . . . 11 (𝐴P𝐴Q)
54pssssd 3666 . . . . . . . . . 10 (𝐴P𝐴Q)
6 ltsonq 9670 . . . . . . . . . 10 <Q Or Q
7 soss 4977 . . . . . . . . . 10 (𝐴Q → ( <Q Or Q → <Q Or 𝐴))
85, 6, 7mpisyl 21 . . . . . . . . 9 (𝐴P → <Q Or 𝐴)
98adantr 480 . . . . . . . 8 ((𝐴P𝐴 ∈ Fin) → <Q Or 𝐴)
10 simpr 476 . . . . . . . 8 ((𝐴P𝐴 ∈ Fin) → 𝐴 ∈ Fin)
11 prn0 9690 . . . . . . . . 9 (𝐴P𝐴 ≠ ∅)
1211adantr 480 . . . . . . . 8 ((𝐴P𝐴 ∈ Fin) → 𝐴 ≠ ∅)
13 fimax2g 8091 . . . . . . . 8 (( <Q Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <Q 𝑦)
149, 10, 12, 13syl3anc 1318 . . . . . . 7 ((𝐴P𝐴 ∈ Fin) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <Q 𝑦)
15 ralnex 2975 . . . . . . . . 9 (∀𝑦𝐴 ¬ 𝑥 <Q 𝑦 ↔ ¬ ∃𝑦𝐴 𝑥 <Q 𝑦)
1615rexbii 3023 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <Q 𝑦 ↔ ∃𝑥𝐴 ¬ ∃𝑦𝐴 𝑥 <Q 𝑦)
17 rexnal 2978 . . . . . . . 8 (∃𝑥𝐴 ¬ ∃𝑦𝐴 𝑥 <Q 𝑦 ↔ ¬ ∀𝑥𝐴𝑦𝐴 𝑥 <Q 𝑦)
1816, 17bitri 263 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <Q 𝑦 ↔ ¬ ∀𝑥𝐴𝑦𝐴 𝑥 <Q 𝑦)
1914, 18sylib 207 . . . . . 6 ((𝐴P𝐴 ∈ Fin) → ¬ ∀𝑥𝐴𝑦𝐴 𝑥 <Q 𝑦)
2019ex 449 . . . . 5 (𝐴P → (𝐴 ∈ Fin → ¬ ∀𝑥𝐴𝑦𝐴 𝑥 <Q 𝑦))
213, 20mt2d 130 . . . 4 (𝐴P → ¬ 𝐴 ∈ Fin)
22 nelne1 2878 . . . 4 ((𝐴 ∈ V ∧ ¬ 𝐴 ∈ Fin) → V ≠ Fin)
231, 21, 22syl2anc 691 . . 3 (𝐴P → V ≠ Fin)
2423necomd 2837 . 2 (𝐴P → Fin ≠ V)
25 fineqv 8060 . . 3 (¬ ω ∈ V ↔ Fin = V)
2625necon1abii 2830 . 2 (Fin ≠ V ↔ ω ∈ V)
2724, 26sylib 207 1 (𝐴P → ω ∈ V)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   Or wor 4958  ωcom 6957  Fincfn 7841  Qcnq 9553
 Copyright terms: Public domain W3C validator