MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolicc2lem5 Structured version   Visualization version   GIF version

Theorem ovolicc2lem5 23725
Description: Lemma for ovolicc2 23726. (Contributed by Mario Carneiro, 14-Jun-2014.)
Hypotheses
Ref Expression
ovolicc.1 (𝜑𝐴 ∈ ℝ)
ovolicc.2 (𝜑𝐵 ∈ ℝ)
ovolicc.3 (𝜑𝐴𝐵)
ovolicc2.4 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ovolicc2.5 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
ovolicc2.6 (𝜑𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
ovolicc2.7 (𝜑 → (𝐴[,]𝐵) ⊆ 𝑈)
ovolicc2.8 (𝜑𝐺:𝑈⟶ℕ)
ovolicc2.9 ((𝜑𝑡𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
ovolicc2.10 𝑇 = {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
Assertion
Ref Expression
ovolicc2lem5 (𝜑 → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Distinct variable groups:   𝑢,𝑡,𝐴   𝑡,𝐵,𝑢   𝑡,𝐹   𝑡,𝐺   𝜑,𝑡   𝑡,𝑇   𝑡,𝑈,𝑢
Allowed substitution hints:   𝜑(𝑢)   𝑆(𝑢,𝑡)   𝑇(𝑢)   𝐹(𝑢)   𝐺(𝑢)

Proof of Theorem ovolicc2lem5
Dummy variables 𝑚 𝑛 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovolicc2.7 . . . 4 (𝜑 → (𝐴[,]𝐵) ⊆ 𝑈)
2 ovolicc.1 . . . . . 6 (𝜑𝐴 ∈ ℝ)
32rexrd 10426 . . . . 5 (𝜑𝐴 ∈ ℝ*)
4 ovolicc.2 . . . . . 6 (𝜑𝐵 ∈ ℝ)
54rexrd 10426 . . . . 5 (𝜑𝐵 ∈ ℝ*)
6 ovolicc.3 . . . . 5 (𝜑𝐴𝐵)
7 lbicc2 12602 . . . . 5 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
83, 5, 6, 7syl3anc 1439 . . . 4 (𝜑𝐴 ∈ (𝐴[,]𝐵))
91, 8sseldd 3822 . . 3 (𝜑𝐴 𝑈)
10 eluni2 4675 . . 3 (𝐴 𝑈 ↔ ∃𝑧𝑈 𝐴𝑧)
119, 10sylib 210 . 2 (𝜑 → ∃𝑧𝑈 𝐴𝑧)
12 ovolicc2.6 . . . . . . . 8 (𝜑𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
13 elin 4019 . . . . . . . 8 (𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin) ↔ (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
1412, 13sylib 210 . . . . . . 7 (𝜑 → (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
1514simprd 491 . . . . . 6 (𝜑𝑈 ∈ Fin)
16 ovolicc2.10 . . . . . . 7 𝑇 = {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
17 ssrab2 3908 . . . . . . 7 {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈
1816, 17eqsstri 3854 . . . . . 6 𝑇𝑈
19 ssfi 8468 . . . . . 6 ((𝑈 ∈ Fin ∧ 𝑇𝑈) → 𝑇 ∈ Fin)
2015, 18, 19sylancl 580 . . . . 5 (𝜑𝑇 ∈ Fin)
211adantr 474 . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐴[,]𝐵) ⊆ 𝑈)
22 inss2 4054 . . . . . . . . . . . . 13 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
23 ovolicc2.8 . . . . . . . . . . . . . . 15 (𝜑𝐺:𝑈⟶ℕ)
24 ineq1 4030 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑡 → (𝑢 ∩ (𝐴[,]𝐵)) = (𝑡 ∩ (𝐴[,]𝐵)))
2524neeq1d 3028 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑡 → ((𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅))
2625, 16elrab2 3576 . . . . . . . . . . . . . . . 16 (𝑡𝑇 ↔ (𝑡𝑈 ∧ (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅))
2726simplbi 493 . . . . . . . . . . . . . . 15 (𝑡𝑇𝑡𝑈)
28 ffvelrn 6621 . . . . . . . . . . . . . . 15 ((𝐺:𝑈⟶ℕ ∧ 𝑡𝑈) → (𝐺𝑡) ∈ ℕ)
2923, 27, 28syl2an 589 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐺𝑡) ∈ ℕ)
30 ovolicc2.5 . . . . . . . . . . . . . . 15 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
3130ffvelrnda 6623 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐺𝑡) ∈ ℕ) → (𝐹‘(𝐺𝑡)) ∈ ( ≤ ∩ (ℝ × ℝ)))
3229, 31syldan 585 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → (𝐹‘(𝐺𝑡)) ∈ ( ≤ ∩ (ℝ × ℝ)))
3322, 32sseldi 3819 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (𝐹‘(𝐺𝑡)) ∈ (ℝ × ℝ))
34 xp2nd 7478 . . . . . . . . . . . 12 ((𝐹‘(𝐺𝑡)) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ)
3533, 34syl 17 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ)
364adantr 474 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 𝐵 ∈ ℝ)
3735, 36ifcld 4352 . . . . . . . . . 10 ((𝜑𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ ℝ)
3826simprbi 492 . . . . . . . . . . . . . 14 (𝑡𝑇 → (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅)
3938adantl 475 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → (𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅)
40 n0 4159 . . . . . . . . . . . . 13 ((𝑡 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))
4139, 40sylib 210 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → ∃𝑦 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))
422adantr 474 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐴 ∈ ℝ)
43 simprr 763 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))
44 elin 4019 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)) ↔ (𝑦𝑡𝑦 ∈ (𝐴[,]𝐵)))
4543, 44sylib 210 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦𝑡𝑦 ∈ (𝐴[,]𝐵)))
4645simprd 491 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ (𝐴[,]𝐵))
474adantr 474 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐵 ∈ ℝ)
48 elicc2 12550 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵)))
4942, 47, 48syl2anc 579 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵)))
5046, 49mpbid 224 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵))
5150simp1d 1133 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ ℝ)
5233adantrr 707 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝐹‘(𝐺𝑡)) ∈ (ℝ × ℝ))
5352, 34syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ)
5450simp2d 1134 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐴𝑦)
5545simpld 490 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦𝑡)
5629adantrr 707 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝐺𝑡) ∈ ℕ)
57 fvco3 6535 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐺𝑡) ∈ ℕ) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = ((,)‘(𝐹‘(𝐺𝑡))))
5830, 57sylan 575 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐺𝑡) ∈ ℕ) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = ((,)‘(𝐹‘(𝐺𝑡))))
5956, 58syldan 585 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = ((,)‘(𝐹‘(𝐺𝑡))))
60 ovolicc2.9 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
6127, 60sylan2 586 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡𝑇) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
6261adantrr 707 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
63 1st2nd2 7484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹‘(𝐺𝑡)) ∈ (ℝ × ℝ) → (𝐹‘(𝐺𝑡)) = ⟨(1st ‘(𝐹‘(𝐺𝑡))), (2nd ‘(𝐹‘(𝐺𝑡)))⟩)
6452, 63syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝐹‘(𝐺𝑡)) = ⟨(1st ‘(𝐹‘(𝐺𝑡))), (2nd ‘(𝐹‘(𝐺𝑡)))⟩)
6564fveq2d 6450 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → ((,)‘(𝐹‘(𝐺𝑡))) = ((,)‘⟨(1st ‘(𝐹‘(𝐺𝑡))), (2nd ‘(𝐹‘(𝐺𝑡)))⟩))
66 df-ov 6925 . . . . . . . . . . . . . . . . . . . . 21 ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))) = ((,)‘⟨(1st ‘(𝐹‘(𝐺𝑡))), (2nd ‘(𝐹‘(𝐺𝑡)))⟩)
6765, 66syl6eqr 2832 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → ((,)‘(𝐹‘(𝐺𝑡))) = ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))))
6859, 62, 673eqtr3d 2822 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑡 = ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))))
6955, 68eleqtrd 2861 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ∈ ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))))
70 xp1st 7477 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝐺𝑡)) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ)
7152, 70syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ)
72 rexr 10422 . . . . . . . . . . . . . . . . . . . 20 ((1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ → (1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ*)
73 rexr 10422 . . . . . . . . . . . . . . . . . . . 20 ((2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ → (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ*)
74 elioo2 12528 . . . . . . . . . . . . . . . . . . . 20 (((1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ* ∧ (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ*) → (𝑦 ∈ ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))) ↔ (𝑦 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑡))) < 𝑦𝑦 < (2nd ‘(𝐹‘(𝐺𝑡))))))
7572, 73, 74syl2an 589 . . . . . . . . . . . . . . . . . . 19 (((1st ‘(𝐹‘(𝐺𝑡))) ∈ ℝ ∧ (2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ) → (𝑦 ∈ ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))) ↔ (𝑦 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑡))) < 𝑦𝑦 < (2nd ‘(𝐹‘(𝐺𝑡))))))
7671, 53, 75syl2anc 579 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ ((1st ‘(𝐹‘(𝐺𝑡)))(,)(2nd ‘(𝐹‘(𝐺𝑡)))) ↔ (𝑦 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑡))) < 𝑦𝑦 < (2nd ‘(𝐹‘(𝐺𝑡))))))
7769, 76mpbid 224 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → (𝑦 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝑡))) < 𝑦𝑦 < (2nd ‘(𝐹‘(𝐺𝑡)))))
7877simp3d 1135 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 < (2nd ‘(𝐹‘(𝐺𝑡))))
7951, 53, 78ltled 10524 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝑦 ≤ (2nd ‘(𝐹‘(𝐺𝑡))))
8042, 51, 53, 54, 79letrd 10533 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑡𝑇𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)))) → 𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡))))
8180expr 450 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → (𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)) → 𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡)))))
8281exlimdv 1976 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (∃𝑦 𝑦 ∈ (𝑡 ∩ (𝐴[,]𝐵)) → 𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡)))))
8341, 82mpd 15 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡))))
846adantr 474 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 𝐴𝐵)
85 breq2 4890 . . . . . . . . . . . 12 ((2nd ‘(𝐹‘(𝐺𝑡))) = if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) → (𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡))) ↔ 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵)))
86 breq2 4890 . . . . . . . . . . . 12 (𝐵 = if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) → (𝐴𝐵𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵)))
8785, 86ifboth 4345 . . . . . . . . . . 11 ((𝐴 ≤ (2nd ‘(𝐹‘(𝐺𝑡))) ∧ 𝐴𝐵) → 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵))
8883, 84, 87syl2anc 579 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵))
89 min2 12333 . . . . . . . . . . 11 (((2nd ‘(𝐹‘(𝐺𝑡))) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ≤ 𝐵)
9035, 36, 89syl2anc 579 . . . . . . . . . 10 ((𝜑𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ≤ 𝐵)
91 elicc2 12550 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵) ↔ (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ ℝ ∧ 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ≤ 𝐵)))
922, 4, 91syl2anc 579 . . . . . . . . . . 11 (𝜑 → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵) ↔ (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ ℝ ∧ 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ≤ 𝐵)))
9392adantr 474 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵) ↔ (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ ℝ ∧ 𝐴 ≤ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ≤ 𝐵)))
9437, 88, 90, 93mpbir3and 1399 . . . . . . . . 9 ((𝜑𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵))
9521, 94sseldd 3822 . . . . . . . 8 ((𝜑𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑈)
96 eluni2 4675 . . . . . . . 8 (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑈 ↔ ∃𝑥𝑈 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)
9795, 96sylib 210 . . . . . . 7 ((𝜑𝑡𝑇) → ∃𝑥𝑈 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)
98 simprl 761 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ (𝑥𝑈 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)) → 𝑥𝑈)
99 simprr 763 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ (𝑥𝑈 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)
10094adantr 474 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ (𝑥𝑈 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵))
101 inelcm 4257 . . . . . . . . 9 ((if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐴[,]𝐵)) → (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅)
10299, 100, 101syl2anc 579 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ (𝑥𝑈 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)) → (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅)
103 ineq1 4030 . . . . . . . . . 10 (𝑢 = 𝑥 → (𝑢 ∩ (𝐴[,]𝐵)) = (𝑥 ∩ (𝐴[,]𝐵)))
104103neeq1d 3028 . . . . . . . . 9 (𝑢 = 𝑥 → ((𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅))
105104, 16elrab2 3576 . . . . . . . 8 (𝑥𝑇 ↔ (𝑥𝑈 ∧ (𝑥 ∩ (𝐴[,]𝐵)) ≠ ∅))
10698, 102, 105sylanbrc 578 . . . . . . 7 (((𝜑𝑡𝑇) ∧ (𝑥𝑈 ∧ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)) → 𝑥𝑇)
10797, 106, 99reximssdv 3200 . . . . . 6 ((𝜑𝑡𝑇) → ∃𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)
108107ralrimiva 3148 . . . . 5 (𝜑 → ∀𝑡𝑇𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥)
109 eleq2 2848 . . . . . 6 (𝑥 = (𝑡) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥 ↔ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)))
110109ac6sfi 8492 . . . . 5 ((𝑇 ∈ Fin ∧ ∀𝑡𝑇𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ 𝑥) → ∃(:𝑇𝑇 ∧ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)))
11120, 108, 110syl2anc 579 . . . 4 (𝜑 → ∃(:𝑇𝑇 ∧ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)))
112111adantr 474 . . 3 ((𝜑 ∧ (𝑧𝑈𝐴𝑧)) → ∃(:𝑇𝑇 ∧ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)))
113 2fveq3 6451 . . . . . . . . . . 11 (𝑥 = 𝑡 → (𝐹‘(𝐺𝑥)) = (𝐹‘(𝐺𝑡)))
114113fveq2d 6450 . . . . . . . . . 10 (𝑥 = 𝑡 → (2nd ‘(𝐹‘(𝐺𝑥))) = (2nd ‘(𝐹‘(𝐺𝑡))))
115114breq1d 4896 . . . . . . . . 9 (𝑥 = 𝑡 → ((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵))
116115, 114ifbieq1d 4330 . . . . . . . 8 (𝑥 = 𝑡 → if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) = if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵))
117 fveq2 6446 . . . . . . . 8 (𝑥 = 𝑡 → (𝑥) = (𝑡))
118116, 117eleq12d 2853 . . . . . . 7 (𝑥 = 𝑡 → (if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥) ↔ if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)))
119118cbvralv 3367 . . . . . 6 (∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥) ↔ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡))
1202adantr 474 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐴 ∈ ℝ)
1214adantr 474 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐵 ∈ ℝ)
1226adantr 474 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐴𝐵)
123 ovolicc2.4 . . . . . . . . 9 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
12430adantr 474 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
12512adantr 474 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
1261adantr 474 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → (𝐴[,]𝐵) ⊆ 𝑈)
12723adantr 474 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐺:𝑈⟶ℕ)
12860adantlr 705 . . . . . . . . 9 (((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) ∧ 𝑡𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
129 simprrl 771 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → :𝑇𝑇)
130 simprrr 772 . . . . . . . . . 10 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥))
131118rspccva 3510 . . . . . . . . . 10 ((∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥) ∧ 𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡))
132130, 131sylan 575 . . . . . . . . 9 (((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) ∧ 𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡))
133 simprlr 770 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐴𝑧)
134 simprll 769 . . . . . . . . . 10 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝑧𝑈)
1358adantr 474 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝐴 ∈ (𝐴[,]𝐵))
136 inelcm 4257 . . . . . . . . . . 11 ((𝐴𝑧𝐴 ∈ (𝐴[,]𝐵)) → (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅)
137133, 135, 136syl2anc 579 . . . . . . . . . 10 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅)
138 ineq1 4030 . . . . . . . . . . . 12 (𝑢 = 𝑧 → (𝑢 ∩ (𝐴[,]𝐵)) = (𝑧 ∩ (𝐴[,]𝐵)))
139138neeq1d 3028 . . . . . . . . . . 11 (𝑢 = 𝑧 → ((𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅ ↔ (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅))
140139, 16elrab2 3576 . . . . . . . . . 10 (𝑧𝑇 ↔ (𝑧𝑈 ∧ (𝑧 ∩ (𝐴[,]𝐵)) ≠ ∅))
141134, 137, 140sylanbrc 578 . . . . . . . . 9 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → 𝑧𝑇)
142 eqid 2778 . . . . . . . . 9 seq1(( ∘ 1st ), (ℕ × {𝑧})) = seq1(( ∘ 1st ), (ℕ × {𝑧}))
143 fveq2 6446 . . . . . . . . . . 11 (𝑚 = 𝑛 → (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑚) = (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑛))
144143eleq2d 2845 . . . . . . . . . 10 (𝑚 = 𝑛 → (𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑚) ↔ 𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑛)))
145144cbvrabv 3396 . . . . . . . . 9 {𝑚 ∈ ℕ ∣ 𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑚)} = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑛)}
146 eqid 2778 . . . . . . . . 9 inf({𝑚 ∈ ℕ ∣ 𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑚)}, ℝ, < ) = inf({𝑚 ∈ ℕ ∣ 𝐵 ∈ (seq1(( ∘ 1st ), (ℕ × {𝑧}))‘𝑚)}, ℝ, < )
147120, 121, 122, 123, 124, 125, 126, 127, 128, 16, 129, 132, 133, 141, 142, 145, 146ovolicc2lem4 23724 . . . . . . . 8 ((𝜑 ∧ ((𝑧𝑈𝐴𝑧) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥)))) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
148147anassrs 461 . . . . . . 7 (((𝜑 ∧ (𝑧𝑈𝐴𝑧)) ∧ (:𝑇𝑇 ∧ ∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥))) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
149148expr 450 . . . . . 6 (((𝜑 ∧ (𝑧𝑈𝐴𝑧)) ∧ :𝑇𝑇) → (∀𝑥𝑇 if((2nd ‘(𝐹‘(𝐺𝑥))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑥))), 𝐵) ∈ (𝑥) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < )))
150119, 149syl5bir 235 . . . . 5 (((𝜑 ∧ (𝑧𝑈𝐴𝑧)) ∧ :𝑇𝑇) → (∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < )))
151150expimpd 447 . . . 4 ((𝜑 ∧ (𝑧𝑈𝐴𝑧)) → ((:𝑇𝑇 ∧ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < )))
152151exlimdv 1976 . . 3 ((𝜑 ∧ (𝑧𝑈𝐴𝑧)) → (∃(:𝑇𝑇 ∧ ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝑡)) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < )))
153112, 152mpd 15 . 2 ((𝜑 ∧ (𝑧𝑈𝐴𝑧)) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
15411, 153rexlimddv 3218 1 (𝜑 → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wex 1823  wcel 2107  wne 2969  wral 3090  wrex 3091  {crab 3094  cin 3791  wss 3792  c0 4141  ifcif 4307  𝒫 cpw 4379  {csn 4398  cop 4404   cuni 4671   class class class wbr 4886   × cxp 5353  ran crn 5356  ccom 5359  wf 6131  cfv 6135  (class class class)co 6922  1st c1st 7443  2nd c2nd 7444  Fincfn 8241  supcsup 8634  infcinf 8635  cr 10271  1c1 10273   + caddc 10275  *cxr 10410   < clt 10411  cle 10412  cmin 10606  cn 11374  (,)cioo 12487  [,]cicc 12490  seqcseq 13119  abscabs 14381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-z 11729  df-uz 11993  df-rp 12138  df-ioo 12491  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-clim 14627  df-sum 14825
This theorem is referenced by:  ovolicc2  23726
  Copyright terms: Public domain W3C validator