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 )