This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )