axpre-sup

Description: A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version with ordering on extended reals is axsup . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup . (Contributed by NM, 19-May-1996) (Revised by Mario Carneiro, 16-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	axpre-sup	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elreal2	⊢ ( 𝑥 ∈ ℝ ↔ ( ( 1^st ‘ 𝑥 ) ∈ R ∧ 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , 0_R ⟩ ) )
2	1	simplbi	⊢ ( 𝑥 ∈ ℝ → ( 1^st ‘ 𝑥 ) ∈ R )
3	2	adantl	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ ) → ( 1^st ‘ 𝑥 ) ∈ R )
4		fo1st	⊢ 1^st : V –onto→ V
5		fof	⊢ ( 1^st : V –onto→ V → 1^st : V ⟶ V )
6		ffn	⊢ ( 1^st : V ⟶ V → 1^st Fn V )
7	4 5 6	mp2b	⊢ 1^st Fn V
8		ssv	⊢ 𝐴 ⊆ V
9		fvelimab	⊢ ( ( 1^st Fn V ∧ 𝐴 ⊆ V ) → ( 𝑤 ∈ ( 1^st “ 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 1^st ‘ 𝑦 ) = 𝑤 ) )
10	7 8 9	mp2an	⊢ ( 𝑤 ∈ ( 1^st “ 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 1^st ‘ 𝑦 ) = 𝑤 )
11		r19.29	⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ( 1^st ‘ 𝑦 ) = 𝑤 ) → ∃ 𝑦 ∈ 𝐴 ( 𝑦 <_ℝ 𝑥 ∧ ( 1^st ‘ 𝑦 ) = 𝑤 ) )
12		ssel2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
13		ltresr2	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦 <_ℝ 𝑥 ↔ ( 1^st ‘ 𝑦 ) <_R ( 1^st ‘ 𝑥 ) ) )
14		breq1	⊢ ( ( 1^st ‘ 𝑦 ) = 𝑤 → ( ( 1^st ‘ 𝑦 ) <_R ( 1^st ‘ 𝑥 ) ↔ 𝑤 <_R ( 1^st ‘ 𝑥 ) ) )
15	13 14	sylan9bb	⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ∧ ( 1^st ‘ 𝑦 ) = 𝑤 ) → ( 𝑦 <_ℝ 𝑥 ↔ 𝑤 <_R ( 1^st ‘ 𝑥 ) ) )
16	15	biimpd	⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ∧ ( 1^st ‘ 𝑦 ) = 𝑤 ) → ( 𝑦 <_ℝ 𝑥 → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) )
17	16	exp31	⊢ ( 𝑦 ∈ ℝ → ( 𝑥 ∈ ℝ → ( ( 1^st ‘ 𝑦 ) = 𝑤 → ( 𝑦 <_ℝ 𝑥 → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) ) ) )
18	12 17	syl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ ℝ → ( ( 1^st ‘ 𝑦 ) = 𝑤 → ( 𝑦 <_ℝ 𝑥 → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) ) ) )
19	18	imp4b	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 1^st ‘ 𝑦 ) = 𝑤 ∧ 𝑦 <_ℝ 𝑥 ) → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) )
20	19	ancomsd	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 <_ℝ 𝑥 ∧ ( 1^st ‘ 𝑦 ) = 𝑤 ) → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) )
21	20	an32s	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑦 <_ℝ 𝑥 ∧ ( 1^st ‘ 𝑦 ) = 𝑤 ) → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) )
22	21	rexlimdva	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑦 <_ℝ 𝑥 ∧ ( 1^st ‘ 𝑦 ) = 𝑤 ) → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) )
23	11 22	syl5	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 ∧ ∃ 𝑦 ∈ 𝐴 ( 1^st ‘ 𝑦 ) = 𝑤 ) → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) )
24	23	expd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 → ( ∃ 𝑦 ∈ 𝐴 ( 1^st ‘ 𝑦 ) = 𝑤 → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) ) )
25	10 24	syl7bi	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 → ( 𝑤 ∈ ( 1^st “ 𝐴 ) → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) ) )
26	25	impr	⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 ) ) → ( 𝑤 ∈ ( 1^st “ 𝐴 ) → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) )
27	26	adantlr	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 ) ) → ( 𝑤 ∈ ( 1^st “ 𝐴 ) → 𝑤 <_R ( 1^st ‘ 𝑥 ) ) )
28	27	ralrimiv	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 ) ) → ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R ( 1^st ‘ 𝑥 ) )
29	28	expr	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 → ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R ( 1^st ‘ 𝑥 ) ) )
30		brralrspcev	⊢ ( ( ( 1^st ‘ 𝑥 ) ∈ R ∧ ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R ( 1^st ‘ 𝑥 ) ) → ∃ 𝑣 ∈ R ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑣 )
31	3 29 30	syl6an	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 → ∃ 𝑣 ∈ R ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑣 ) )
32	31	rexlimdva	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 → ∃ 𝑣 ∈ R ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑣 ) )
33		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 )
34		fnfvima	⊢ ( ( 1^st Fn V ∧ 𝐴 ⊆ V ∧ 𝑦 ∈ 𝐴 ) → ( 1^st ‘ 𝑦 ) ∈ ( 1^st “ 𝐴 ) )
35	7 8 34	mp3an12	⊢ ( 𝑦 ∈ 𝐴 → ( 1^st ‘ 𝑦 ) ∈ ( 1^st “ 𝐴 ) )
36	35	ne0d	⊢ ( 𝑦 ∈ 𝐴 → ( 1^st “ 𝐴 ) ≠ ∅ )
37	36	exlimiv	⊢ ( ∃ 𝑦 𝑦 ∈ 𝐴 → ( 1^st “ 𝐴 ) ≠ ∅ )
38	33 37	sylbi	⊢ ( 𝐴 ≠ ∅ → ( 1^st “ 𝐴 ) ≠ ∅ )
39		supsr	⊢ ( ( ( 1^st “ 𝐴 ) ≠ ∅ ∧ ∃ 𝑣 ∈ R ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑣 ) → ∃ 𝑣 ∈ R ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 ∧ ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) ) )
40	39	ex	⊢ ( ( 1^st “ 𝐴 ) ≠ ∅ → ( ∃ 𝑣 ∈ R ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑣 → ∃ 𝑣 ∈ R ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 ∧ ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) ) ) )
41	38 40	syl	⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑣 ∈ R ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑣 → ∃ 𝑣 ∈ R ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 ∧ ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) ) ) )
42	41	adantl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑣 ∈ R ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑣 → ∃ 𝑣 ∈ R ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 ∧ ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) ) ) )
43		breq2	⊢ ( 𝑤 = ( 1^st ‘ 𝑦 ) → ( 𝑣 <_R 𝑤 ↔ 𝑣 <_R ( 1^st ‘ 𝑦 ) ) )
44	43	notbid	⊢ ( 𝑤 = ( 1^st ‘ 𝑦 ) → ( ¬ 𝑣 <_R 𝑤 ↔ ¬ 𝑣 <_R ( 1^st ‘ 𝑦 ) ) )
45	44	rspccv	⊢ ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 → ( ( 1^st ‘ 𝑦 ) ∈ ( 1^st “ 𝐴 ) → ¬ 𝑣 <_R ( 1^st ‘ 𝑦 ) ) )
46	35 45	syl5com	⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 → ¬ 𝑣 <_R ( 1^st ‘ 𝑦 ) ) )
47	46	adantl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 → ¬ 𝑣 <_R ( 1^st ‘ 𝑦 ) ) )
48		elreal2	⊢ ( 𝑦 ∈ ℝ ↔ ( ( 1^st ‘ 𝑦 ) ∈ R ∧ 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , 0_R ⟩ ) )
49	48	simprbi	⊢ ( 𝑦 ∈ ℝ → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , 0_R ⟩ )
50	49	breq2d	⊢ ( 𝑦 ∈ ℝ → ( ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ↔ ⟨ 𝑣 , 0_R ⟩ <_ℝ ⟨ ( 1^st ‘ 𝑦 ) , 0_R ⟩ ) )
51		ltresr	⊢ ( ⟨ 𝑣 , 0_R ⟩ <_ℝ ⟨ ( 1^st ‘ 𝑦 ) , 0_R ⟩ ↔ 𝑣 <_R ( 1^st ‘ 𝑦 ) )
52	50 51	bitrdi	⊢ ( 𝑦 ∈ ℝ → ( ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ↔ 𝑣 <_R ( 1^st ‘ 𝑦 ) ) )
53	12 52	syl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → ( ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ↔ 𝑣 <_R ( 1^st ‘ 𝑦 ) ) )
54	53	notbid	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → ( ¬ ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ↔ ¬ 𝑣 <_R ( 1^st ‘ 𝑦 ) ) )
55	47 54	sylibrd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 → ¬ ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ) )
56	55	ralrimdva	⊢ ( 𝐴 ⊆ ℝ → ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 → ∀ 𝑦 ∈ 𝐴 ¬ ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ) )
57	56	ad2antrr	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣 ∈ R ) → ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 → ∀ 𝑦 ∈ 𝐴 ¬ ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ) )
58	49	breq1d	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ ↔ ⟨ ( 1^st ‘ 𝑦 ) , 0_R ⟩ <_ℝ ⟨ 𝑣 , 0_R ⟩ ) )
59		ltresr	⊢ ( ⟨ ( 1^st ‘ 𝑦 ) , 0_R ⟩ <_ℝ ⟨ 𝑣 , 0_R ⟩ ↔ ( 1^st ‘ 𝑦 ) <_R 𝑣 )
60	58 59	bitrdi	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ ↔ ( 1^st ‘ 𝑦 ) <_R 𝑣 ) )
61	48	simplbi	⊢ ( 𝑦 ∈ ℝ → ( 1^st ‘ 𝑦 ) ∈ R )
62		breq1	⊢ ( 𝑤 = ( 1^st ‘ 𝑦 ) → ( 𝑤 <_R 𝑣 ↔ ( 1^st ‘ 𝑦 ) <_R 𝑣 ) )
63		breq1	⊢ ( 𝑤 = ( 1^st ‘ 𝑦 ) → ( 𝑤 <_R 𝑢 ↔ ( 1^st ‘ 𝑦 ) <_R 𝑢 ) )
64	63	rexbidv	⊢ ( 𝑤 = ( 1^st ‘ 𝑦 ) → ( ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ↔ ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) ( 1^st ‘ 𝑦 ) <_R 𝑢 ) )
65	62 64	imbi12d	⊢ ( 𝑤 = ( 1^st ‘ 𝑦 ) → ( ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) ↔ ( ( 1^st ‘ 𝑦 ) <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) ( 1^st ‘ 𝑦 ) <_R 𝑢 ) ) )
66	65	rspccv	⊢ ( ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) → ( ( 1^st ‘ 𝑦 ) ∈ R → ( ( 1^st ‘ 𝑦 ) <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) ( 1^st ‘ 𝑦 ) <_R 𝑢 ) ) )
67	61 66	syl5	⊢ ( ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) → ( 𝑦 ∈ ℝ → ( ( 1^st ‘ 𝑦 ) <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) ( 1^st ‘ 𝑦 ) <_R 𝑢 ) ) )
68	67	com3l	⊢ ( 𝑦 ∈ ℝ → ( ( 1^st ‘ 𝑦 ) <_R 𝑣 → ( ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) ( 1^st ‘ 𝑦 ) <_R 𝑢 ) ) )
69	60 68	sylbid	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ( ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) ( 1^st ‘ 𝑦 ) <_R 𝑢 ) ) )
70	69	adantr	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ( ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) ( 1^st ‘ 𝑦 ) <_R 𝑢 ) ) )
71		fvelimab	⊢ ( ( 1^st Fn V ∧ 𝐴 ⊆ V ) → ( 𝑢 ∈ ( 1^st “ 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐴 ( 1^st ‘ 𝑧 ) = 𝑢 ) )
72	7 8 71	mp2an	⊢ ( 𝑢 ∈ ( 1^st “ 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐴 ( 1^st ‘ 𝑧 ) = 𝑢 )
73		ssel2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
74		ltresr2	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 <_ℝ 𝑧 ↔ ( 1^st ‘ 𝑦 ) <_R ( 1^st ‘ 𝑧 ) ) )
75	73 74	sylan2	⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 <_ℝ 𝑧 ↔ ( 1^st ‘ 𝑦 ) <_R ( 1^st ‘ 𝑧 ) ) )
76		breq2	⊢ ( ( 1^st ‘ 𝑧 ) = 𝑢 → ( ( 1^st ‘ 𝑦 ) <_R ( 1^st ‘ 𝑧 ) ↔ ( 1^st ‘ 𝑦 ) <_R 𝑢 ) )
77	75 76	sylan9bb	⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 1^st ‘ 𝑧 ) = 𝑢 ) → ( 𝑦 <_ℝ 𝑧 ↔ ( 1^st ‘ 𝑦 ) <_R 𝑢 ) )
78	77	exbiri	⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 1^st ‘ 𝑧 ) = 𝑢 → ( ( 1^st ‘ 𝑦 ) <_R 𝑢 → 𝑦 <_ℝ 𝑧 ) ) )
79	78	expr	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝑧 ∈ 𝐴 → ( ( 1^st ‘ 𝑧 ) = 𝑢 → ( ( 1^st ‘ 𝑦 ) <_R 𝑢 → 𝑦 <_ℝ 𝑧 ) ) ) )
80	79	com4r	⊢ ( ( 1^st ‘ 𝑦 ) <_R 𝑢 → ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝑧 ∈ 𝐴 → ( ( 1^st ‘ 𝑧 ) = 𝑢 → 𝑦 <_ℝ 𝑧 ) ) ) )
81	80	imp	⊢ ( ( ( 1^st ‘ 𝑦 ) <_R 𝑢 ∧ ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) ) → ( 𝑧 ∈ 𝐴 → ( ( 1^st ‘ 𝑧 ) = 𝑢 → 𝑦 <_ℝ 𝑧 ) ) )
82	81	reximdvai	⊢ ( ( ( 1^st ‘ 𝑦 ) <_R 𝑢 ∧ ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) ) → ( ∃ 𝑧 ∈ 𝐴 ( 1^st ‘ 𝑧 ) = 𝑢 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) )
83	72 82	syl5bi	⊢ ( ( ( 1^st ‘ 𝑦 ) <_R 𝑢 ∧ ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) ) → ( 𝑢 ∈ ( 1^st “ 𝐴 ) → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) )
84	83	expcom	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ( 1^st ‘ 𝑦 ) <_R 𝑢 → ( 𝑢 ∈ ( 1^st “ 𝐴 ) → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) )
85	84	com23	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝑢 ∈ ( 1^st “ 𝐴 ) → ( ( 1^st ‘ 𝑦 ) <_R 𝑢 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) )
86	85	rexlimdv	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) ( 1^st ‘ 𝑦 ) <_R 𝑢 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) )
87	70 86	syl6d	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ( ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) )
88	87	com23	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) → ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) )
89	88	ex	⊢ ( 𝑦 ∈ ℝ → ( 𝐴 ⊆ ℝ → ( ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) → ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) ) )
90	89	com3l	⊢ ( 𝐴 ⊆ ℝ → ( ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) → ( 𝑦 ∈ ℝ → ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) ) )
91	90	ad2antrr	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣 ∈ R ) → ( ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) → ( 𝑦 ∈ ℝ → ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) ) )
92	91	ralrimdv	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣 ∈ R ) → ( ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) → ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) )
93		opelreal	⊢ ( ⟨ 𝑣 , 0_R ⟩ ∈ ℝ ↔ 𝑣 ∈ R )
94	93	biimpri	⊢ ( 𝑣 ∈ R → ⟨ 𝑣 , 0_R ⟩ ∈ ℝ )
95	94	adantl	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣 ∈ R ) → ⟨ 𝑣 , 0_R ⟩ ∈ ℝ )
96		breq1	⊢ ( 𝑥 = ⟨ 𝑣 , 0_R ⟩ → ( 𝑥 <_ℝ 𝑦 ↔ ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ) )
97	96	notbid	⊢ ( 𝑥 = ⟨ 𝑣 , 0_R ⟩ → ( ¬ 𝑥 <_ℝ 𝑦 ↔ ¬ ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ) )
98	97	ralbidv	⊢ ( 𝑥 = ⟨ 𝑣 , 0_R ⟩ → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <_ℝ 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ) )
99		breq2	⊢ ( 𝑥 = ⟨ 𝑣 , 0_R ⟩ → ( 𝑦 <_ℝ 𝑥 ↔ 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ ) )
100	99	imbi1d	⊢ ( 𝑥 = ⟨ 𝑣 , 0_R ⟩ → ( ( 𝑦 <_ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ↔ ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) )
101	100	ralbidv	⊢ ( 𝑥 = ⟨ 𝑣 , 0_R ⟩ → ( ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) )
102	98 101	anbi12d	⊢ ( 𝑥 = ⟨ 𝑣 , 0_R ⟩ → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) ) )
103	102	rspcev	⊢ ( ( ⟨ 𝑣 , 0_R ⟩ ∈ ℝ ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) )
104	103	ex	⊢ ( ⟨ 𝑣 , 0_R ⟩ ∈ ℝ → ( ( ∀ 𝑦 ∈ 𝐴 ¬ ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) ) )
105	95 104	syl	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣 ∈ R ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ ⟨ 𝑣 , 0_R ⟩ <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ ⟨ 𝑣 , 0_R ⟩ → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) ) )
106	57 92 105	syl2and	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣 ∈ R ) → ( ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 ∧ ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) ) )
107	106	rexlimdva	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑣 ∈ R ( ∀ 𝑤 ∈ ( 1^st “ 𝐴 ) ¬ 𝑣 <_R 𝑤 ∧ ∀ 𝑤 ∈ R ( 𝑤 <_R 𝑣 → ∃ 𝑢 ∈ ( 1^st “ 𝐴 ) 𝑤 <_R 𝑢 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) ) )
108	32 42 107	3syld	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) ) )
109	108	3impia	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <_ℝ 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <_ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <_ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <_ℝ 𝑧 ) ) )

Metamath Proof Explorer

Theorem axpre-sup

Proof