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

Metamath Proof Explorer

Theorem zsupss

Description: Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup .) (Contributed by Mario Carneiro, 21-Apr-2015)

Ref Expression
Assertion zsupss ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑦 = 𝑚 → ( 𝑦 ≤ 𝑥 ↔ 𝑚 ≤ 𝑥 ) )
2 1 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑥 )
3 breq2 ⊢ ( 𝑥 = 𝑛 → ( 𝑚 ≤ 𝑥 ↔ 𝑚 ≤ 𝑛 ) )
4 3 ralbidv ⊢ ( 𝑥 = 𝑛 → ( ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑥 ↔ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) )
5 2 4 bitrid ⊢ ( 𝑥 = 𝑛 → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) )
6 5 cbvrexvw ⊢ ( ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∃ 𝑛 ∈ ℤ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 )
7 simp1rl ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) → 𝑛 ∈ ℤ )
8 7 znegcld ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) → - 𝑛 ∈ ℤ )
9 simp2 ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ℤ )
10 9 zred ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ℝ )
11 7 zred ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) → 𝑛 ∈ ℝ )
12 breq1 ⊢ ( 𝑚 = - 𝑤 → ( 𝑚 ≤ 𝑛 ↔ - 𝑤 ≤ 𝑛 ) )
13 simp1rr ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) → ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 )
14 simp3 ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) → - 𝑤 ∈ 𝐴 )
15 12 13 14 rspcdva ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) → - 𝑤 ≤ 𝑛 )
16 10 11 15 lenegcon1d ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) → - 𝑛 ≤ 𝑤 )
17 eluz2 ⊢ ( 𝑤 ∈ ( ℤ≥ ‘ - 𝑛 ) ↔ ( - 𝑛 ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ - 𝑛 ≤ 𝑤 ) )
18 8 9 16 17 syl3anbrc ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑤 ∈ ℤ ∧ - 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ( ℤ≥ ‘ - 𝑛 ) )
19 18 rabssdv ⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) → { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } ⊆ ( ℤ≥ ‘ - 𝑛 ) )
20 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑛 𝑛 ∈ 𝐴 )
21 ssel2 ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑛 ∈ 𝐴 ) → 𝑛 ∈ ℤ )
22 21 znegcld ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑛 ∈ 𝐴 ) → - 𝑛 ∈ ℤ )
23 21 zcnd ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑛 ∈ 𝐴 ) → 𝑛 ∈ ℂ )
24 23 negnegd ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑛 ∈ 𝐴 ) → - - 𝑛 = 𝑛 )
25 simpr ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑛 ∈ 𝐴 ) → 𝑛 ∈ 𝐴 )
26 24 25 eqeltrd ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑛 ∈ 𝐴 ) → - - 𝑛 ∈ 𝐴 )
27 negeq ⊢ ( 𝑤 = - 𝑛 → - 𝑤 = - - 𝑛 )
28 27 eleq1d ⊢ ( 𝑤 = - 𝑛 → ( - 𝑤 ∈ 𝐴 ↔ - - 𝑛 ∈ 𝐴 ) )
29 28 rspcev ⊢ ( ( - 𝑛 ∈ ℤ ∧ - - 𝑛 ∈ 𝐴 ) → ∃ 𝑤 ∈ ℤ - 𝑤 ∈ 𝐴 )
30 22 26 29 syl2anc ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑛 ∈ 𝐴 ) → ∃ 𝑤 ∈ ℤ - 𝑤 ∈ 𝐴 )
31 30 ex ⊢ ( 𝐴 ⊆ ℤ → ( 𝑛 ∈ 𝐴 → ∃ 𝑤 ∈ ℤ - 𝑤 ∈ 𝐴 ) )
32 31 exlimdv ⊢ ( 𝐴 ⊆ ℤ → ( ∃ 𝑛 𝑛 ∈ 𝐴 → ∃ 𝑤 ∈ ℤ - 𝑤 ∈ 𝐴 ) )
33 32 imp ⊢ ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑛 𝑛 ∈ 𝐴 ) → ∃ 𝑤 ∈ ℤ - 𝑤 ∈ 𝐴 )
34 20 33 sylan2b ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) → ∃ 𝑤 ∈ ℤ - 𝑤 ∈ 𝐴 )
35 34 adantr ⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) → ∃ 𝑤 ∈ ℤ - 𝑤 ∈ 𝐴 )
36 rabn0 ⊢ ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } ≠ ∅ ↔ ∃ 𝑤 ∈ ℤ - 𝑤 ∈ 𝐴 )
37 35 36 sylibr ⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) → { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } ≠ ∅ )
38 infssuzcl ⊢ ( ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } ⊆ ( ℤ≥ ‘ - 𝑛 ) ∧ { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } ≠ ∅ ) → inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } )
39 19 37 38 syl2anc ⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) → inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } )
40 negeq ⊢ ( 𝑛 = inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → - 𝑛 = - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) )
41 40 eleq1d ⊢ ( 𝑛 = inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ( - 𝑛 ∈ 𝐴 ↔ - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ 𝐴 ) )
42 negeq ⊢ ( 𝑤 = 𝑛 → - 𝑤 = - 𝑛 )
43 42 eleq1d ⊢ ( 𝑤 = 𝑛 → ( - 𝑤 ∈ 𝐴 ↔ - 𝑛 ∈ 𝐴 ) )
44 43 cbvrabv ⊢ { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } = { 𝑛 ∈ ℤ ∣ - 𝑛 ∈ 𝐴 }
45 41 44 elrab2 ⊢ ( inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } ↔ ( inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ ℤ ∧ - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ 𝐴 ) )
46 45 simprbi ⊢ ( inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } → - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ 𝐴 )
47 39 46 syl ⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) → - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ 𝐴 )
48 simpll ⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) → 𝐴 ⊆ ℤ )
49 48 sselda ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℤ )
50 49 zred ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
51 ssrab2 ⊢ { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } ⊆ ℤ
52 39 adantr ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } )
53 51 52 sselid ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ ℤ )
54 53 znegcld ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ ℤ )
55 54 zred ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ ℝ )
56 53 zred ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ ℝ )
57 19 adantr ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } ⊆ ( ℤ≥ ‘ - 𝑛 ) )
58 negeq ⊢ ( 𝑤 = - 𝑦 → - 𝑤 = - - 𝑦 )
59 58 eleq1d ⊢ ( 𝑤 = - 𝑦 → ( - 𝑤 ∈ 𝐴 ↔ - - 𝑦 ∈ 𝐴 ) )
60 49 znegcld ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → - 𝑦 ∈ ℤ )
61 49 zcnd ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℂ )
62 61 negnegd ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → - - 𝑦 = 𝑦 )
63 simpr ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
64 62 63 eqeltrd ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → - - 𝑦 ∈ 𝐴 )
65 59 60 64 elrabd ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → - 𝑦 ∈ { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } )
66 infssuzle ⊢ ( ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } ⊆ ( ℤ≥ ‘ - 𝑛 ) ∧ - 𝑦 ∈ { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } ) → inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ≤ - 𝑦 )
67 57 65 66 syl2anc ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ≤ - 𝑦 )
68 56 50 67 lenegcon2d ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ≤ - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) )
69 50 55 68 lensymd ⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → ¬ - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) < 𝑦 )
70 69 ralrimiva ⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) → ∀ 𝑦 ∈ 𝐴 ¬ - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) < 𝑦 )
71 breq2 ⊢ ( 𝑧 = - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ( 𝑦 < 𝑧 ↔ 𝑦 < - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ) )
72 71 rspcev ⊢ ( ( - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ 𝐴 ∧ 𝑦 < - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 )
73 72 ex ⊢ ( - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ 𝐴 → ( 𝑦 < - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
74 47 73 syl ⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) → ( 𝑦 < - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
75 74 ralrimivw ⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) → ∀ 𝑦 ∈ 𝐵 ( 𝑦 < - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) )
76 breq1 ⊢ ( 𝑥 = - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ( 𝑥 < 𝑦 ↔ - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) < 𝑦 ) )
77 76 notbid ⊢ ( 𝑥 = - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ( ¬ 𝑥 < 𝑦 ↔ ¬ - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) < 𝑦 ) )
78 77 ralbidv ⊢ ( 𝑥 = - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) < 𝑦 ) )
79 breq2 ⊢ ( 𝑥 = - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ( 𝑦 < 𝑥 ↔ 𝑦 < - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ) )
80 79 imbi1d ⊢ ( 𝑥 = - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ( 𝑦 < - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
81 80 ralbidv ⊢ ( 𝑥 = - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑦 < - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
82 78 81 anbi12d ⊢ ( 𝑥 = - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) < 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 < - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
83 82 rspcev ⊢ ( ( - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) < 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 < - inf ( { 𝑤 ∈ ℤ ∣ - 𝑤 ∈ 𝐴 } , ℝ , < ) → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
84 47 70 75 83 syl12anc ⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑛 ∈ ℤ ∧ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
85 84 rexlimdvaa ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑛 ∈ ℤ ∀ 𝑚 ∈ 𝐴 𝑚 ≤ 𝑛 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
86 6 85 biimtrid ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
87 86 3impia ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )