Theorem dedekind

Description: The Dedekind cut theorem. This theorem, which may be used to replace ax-pre-sup with appropriate adjustments, states that, if A completely preceeds B , then there is some number separating the two of them. (Contributed by Scott Fenton, 13-Jun-2013)

	Ref	Expression
Assertion	dedekind	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑥 ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ )
2		nfv	⊢ Ⅎ 𝑥 ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ )
3		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦
4	1 2 3	nf3an	⊢ Ⅎ 𝑥 ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 )
5		nfv	⊢ Ⅎ 𝑥 𝑧 ∈ ℝ
6		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥
7		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 )
8	6 7	nfan	⊢ Ⅎ 𝑥 ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) )
9	5 8	nfan	⊢ Ⅎ 𝑥 ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) )
10	4 9	nfan	⊢ Ⅎ 𝑥 ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) )
11		nfv	⊢ Ⅎ 𝑦 ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ )
12		nfv	⊢ Ⅎ 𝑦 ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ )
13		nfra2w	⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦
14	11 12 13	nf3an	⊢ Ⅎ 𝑦 ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 )
15		nfv	⊢ Ⅎ 𝑦 ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) )
16	14 15	nfan	⊢ Ⅎ 𝑦 ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) )
17		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
18		simpl2l	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) → 𝐴 ⊆ ℝ )
19	18	sselda	⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
20		simplrl	⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
21		simprrl	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) → ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 )
22	21	r19.21bi	⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑧 < 𝑥 )
23	19 20 22	nltled	⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ 𝑧 )
24	23	ex	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) → ( 𝑥 ∈ 𝐴 → 𝑥 ≤ 𝑧 ) )
25		simprll	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑧 ∈ ℝ )
26		simp2r	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → 𝐵 ⊆ ℝ )
27		simpr	⊢ ( ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
28		ssel2	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℝ )
29	26 27 28	syl2an	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ℝ )
30		simpl3	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 )
31		simp2	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) )
32		rsp	⊢ ( ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 → ( 𝑦 ∈ 𝐵 → 𝑥 < 𝑦 ) )
33	32	com12	⊢ ( 𝑦 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 → 𝑥 < 𝑦 ) )
34	33	adantl	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 → 𝑥 < 𝑦 ) )
35		ssel2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
36	35	adantlr	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
37		simplr	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ ℝ )
38	37	sselda	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℝ )
39		ltnsym	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 < 𝑦 → ¬ 𝑦 < 𝑥 ) )
40	36 38 39	syl2an2r	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 < 𝑦 → ¬ 𝑦 < 𝑥 ) )
41	34 40	syld	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 → ¬ 𝑦 < 𝑥 ) )
42	41	an32s	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 → ¬ 𝑦 < 𝑥 ) )
43	42	ralimdva	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 → ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 < 𝑥 ) )
44	31 27 43	syl2an	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 → ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 < 𝑥 ) )
45	30 44	mpd	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 < 𝑥 )
46		breq2	⊢ ( 𝑥 = 𝑤 → ( 𝑦 < 𝑥 ↔ 𝑦 < 𝑤 ) )
47	46	notbid	⊢ ( 𝑥 = 𝑤 → ( ¬ 𝑦 < 𝑥 ↔ ¬ 𝑦 < 𝑤 ) )
48	47	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑦 < 𝑥 ↔ ∀ 𝑤 ∈ 𝐴 ¬ 𝑦 < 𝑤 )
49	45 48	sylib	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ∀ 𝑤 ∈ 𝐴 ¬ 𝑦 < 𝑤 )
50		ralnex	⊢ ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑦 < 𝑤 ↔ ¬ ∃ 𝑤 ∈ 𝐴 𝑦 < 𝑤 )
51	49 50	sylib	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ¬ ∃ 𝑤 ∈ 𝐴 𝑦 < 𝑤 )
52		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 < 𝑧 ↔ 𝑦 < 𝑧 ) )
53		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 < 𝑤 ↔ 𝑦 < 𝑤 ) )
54	53	rexbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ↔ ∃ 𝑤 ∈ 𝐴 𝑦 < 𝑤 ) )
55	52 54	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ↔ ( 𝑦 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑦 < 𝑤 ) ) )
56		simplrr	⊢ ( ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) )
57	56	adantl	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) )
58	55 57 29	rspcdva	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑦 < 𝑤 ) )
59	51 58	mtod	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ¬ 𝑦 < 𝑧 )
60	25 29 59	nltled	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑧 ≤ 𝑦 )
61	60	expr	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) → ( 𝑦 ∈ 𝐵 → 𝑧 ≤ 𝑦 ) )
62	24 61	anim12d	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) ) )
63	62	expd	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) ) ) )
64	16 17 63	ralrimd	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) → ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) ) )
65	10 64	ralrimi	⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) ∧ ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )
66		simp2l	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → 𝐴 ⊆ ℝ )
67		simp1l	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → 𝐴 ≠ ∅ )
68		simp1r	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → 𝐵 ≠ ∅ )
69		n0	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐵 )
70	68 69	sylib	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 𝑧 ∈ 𝐵 )
71	26	sseld	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ℝ ) )
72		ralcom	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑦 )
73		breq2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 < 𝑦 ↔ 𝑥 < 𝑧 ) )
74	73	ralbidv	⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑧 ) )
75	74	rspccv	⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑦 → ( 𝑧 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑧 ) )
76	72 75	sylbi	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 → ( 𝑧 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑧 ) )
77	76	3ad2ant3	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ( 𝑧 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑧 ) )
78	71 77	jcad	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ( 𝑧 ∈ 𝐵 → ( 𝑧 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑧 ) ) )
79	78	eximdv	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ( ∃ 𝑧 𝑧 ∈ 𝐵 → ∃ 𝑧 ( 𝑧 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑧 ) ) )
80	70 79	mpd	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 ( 𝑧 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑧 ) )
81		df-rex	⊢ ( ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑧 ↔ ∃ 𝑧 ( 𝑧 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑧 ) )
82	80 81	sylibr	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑧 )
83		axsup	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 < 𝑧 ) → ∃ 𝑧 ∈ ℝ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) )
84	66 67 82 83	syl3anc	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 ∈ ℝ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑧 < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < 𝑧 → ∃ 𝑤 ∈ 𝐴 𝑥 < 𝑤 ) ) )
85	65 84	reximddv	⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )
86	85	3expib	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) ) )
87		1re	⊢ 1 ∈ ℝ
88		rzal	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 1 ∧ 1 ≤ 𝑦 ) )
89		breq2	⊢ ( 𝑧 = 1 → ( 𝑥 ≤ 𝑧 ↔ 𝑥 ≤ 1 ) )
90		breq1	⊢ ( 𝑧 = 1 → ( 𝑧 ≤ 𝑦 ↔ 1 ≤ 𝑦 ) )
91	89 90	anbi12d	⊢ ( 𝑧 = 1 → ( ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) ↔ ( 𝑥 ≤ 1 ∧ 1 ≤ 𝑦 ) ) )
92	91	2ralbidv	⊢ ( 𝑧 = 1 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 1 ∧ 1 ≤ 𝑦 ) ) )
93	92	rspcev	⊢ ( ( 1 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 1 ∧ 1 ≤ 𝑦 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )
94	87 88 93	sylancr	⊢ ( 𝐴 = ∅ → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )
95	94	a1d	⊢ ( 𝐴 = ∅ → ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) ) )
96		rzal	⊢ ( 𝐵 = ∅ → ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 1 ∧ 1 ≤ 𝑦 ) )
97	96	ralrimivw	⊢ ( 𝐵 = ∅ → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 1 ∧ 1 ≤ 𝑦 ) )
98	87 97 93	sylancr	⊢ ( 𝐵 = ∅ → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )
99	98	a1d	⊢ ( 𝐵 = ∅ → ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) ) )
100	86 95 99	pm2.61iine	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )
101	100	3impa	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )