Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ioorrnopnxrlem Structured version   Visualization version   GIF version

Theorem ioorrnopnxrlem 42047
Description: Given a point 𝐹 that belongs to an indexed product of (possibly unbounded) open intervals, then 𝐹 belongs to an open product of bounded open intervals that's a subset of the original indexed product. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
Hypotheses
Ref Expression
ioorrnopnxrlem.x (𝜑𝑋 ∈ Fin)
ioorrnopnxrlem.a (𝜑𝐴:𝑋⟶ℝ*)
ioorrnopnxrlem.b (𝜑𝐵:𝑋⟶ℝ*)
ioorrnopnxrlem.f (𝜑𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
ioorrnopnxrlem.l 𝐿 = (𝑖𝑋 ↦ if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)))
ioorrnopnxrlem.r 𝑅 = (𝑖𝑋 ↦ if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)))
ioorrnopnxrlem.v 𝑉 = X𝑖𝑋 ((𝐿𝑖)(,)(𝑅𝑖))
Assertion
Ref Expression
ioorrnopnxrlem (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
Distinct variable groups:   𝑣,𝐴   𝑣,𝐵   𝑖,𝐹,𝑣   𝑖,𝐿   𝑅,𝑖   𝑣,𝑉   𝑖,𝑋,𝑣   𝜑,𝑖
Allowed substitution hints:   𝜑(𝑣)   𝐴(𝑖)   𝐵(𝑖)   𝑅(𝑣)   𝐿(𝑣)   𝑉(𝑖)

Proof of Theorem ioorrnopnxrlem
StepHypRef Expression
1 ioorrnopnxrlem.v . . . 4 𝑉 = X𝑖𝑋 ((𝐿𝑖)(,)(𝑅𝑖))
21a1i 11 . . 3 (𝜑𝑉 = X𝑖𝑋 ((𝐿𝑖)(,)(𝑅𝑖)))
3 ioorrnopnxrlem.x . . . 4 (𝜑𝑋 ∈ Fin)
4 iftrue 4350 . . . . . . . 8 ((𝐴𝑖) = -∞ → if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)) = ((𝐹𝑖) − 1))
54adantl 474 . . . . . . 7 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)) = ((𝐹𝑖) − 1))
6 ioorrnopnxrlem.f . . . . . . . . . . . 12 (𝜑𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
76adantr 473 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → 𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
8 simpr 477 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → 𝑖𝑋)
9 fvixp2 40912 . . . . . . . . . . 11 ((𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ∧ 𝑖𝑋) → (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
107, 8, 9syl2anc 576 . . . . . . . . . 10 ((𝜑𝑖𝑋) → (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖)))
1110elioored 41281 . . . . . . . . 9 ((𝜑𝑖𝑋) → (𝐹𝑖) ∈ ℝ)
12 1red 10438 . . . . . . . . 9 ((𝜑𝑖𝑋) → 1 ∈ ℝ)
1311, 12resubcld 10867 . . . . . . . 8 ((𝜑𝑖𝑋) → ((𝐹𝑖) − 1) ∈ ℝ)
1413adantr 473 . . . . . . 7 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → ((𝐹𝑖) − 1) ∈ ℝ)
155, 14eqeltrd 2860 . . . . . 6 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)) ∈ ℝ)
16 iffalse 4353 . . . . . . . 8 (¬ (𝐴𝑖) = -∞ → if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)) = (𝐴𝑖))
1716adantl 474 . . . . . . 7 (((𝜑𝑖𝑋) ∧ ¬ (𝐴𝑖) = -∞) → if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)) = (𝐴𝑖))
18 neqne 2969 . . . . . . . . 9 (¬ (𝐴𝑖) = -∞ → (𝐴𝑖) ≠ -∞)
1918adantl 474 . . . . . . . 8 (((𝜑𝑖𝑋) ∧ ¬ (𝐴𝑖) = -∞) → (𝐴𝑖) ≠ -∞)
20 ioorrnopnxrlem.a . . . . . . . . . . 11 (𝜑𝐴:𝑋⟶ℝ*)
2120ffvelrnda 6674 . . . . . . . . . 10 ((𝜑𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
2221adantr 473 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) ≠ -∞) → (𝐴𝑖) ∈ ℝ*)
23 simpr 477 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) ≠ -∞) → (𝐴𝑖) ≠ -∞)
24 pnfxr 10492 . . . . . . . . . . . 12 +∞ ∈ ℝ*
2524a1i 11 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → +∞ ∈ ℝ*)
2611rexrd 10488 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (𝐹𝑖) ∈ ℝ*)
27 ioorrnopnxrlem.b . . . . . . . . . . . . . 14 (𝜑𝐵:𝑋⟶ℝ*)
2827ffvelrnda 6674 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
29 ioogtlb 41226 . . . . . . . . . . . . 13 (((𝐴𝑖) ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))) → (𝐴𝑖) < (𝐹𝑖))
3021, 28, 10, 29syl3anc 1351 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (𝐴𝑖) < (𝐹𝑖))
3111ltpnfd 12331 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (𝐹𝑖) < +∞)
3221, 26, 25, 30, 31xrlttrd 12367 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝐴𝑖) < +∞)
3321, 25, 32xrltned 41079 . . . . . . . . . 10 ((𝜑𝑖𝑋) → (𝐴𝑖) ≠ +∞)
3433adantr 473 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) ≠ -∞) → (𝐴𝑖) ≠ +∞)
3522, 23, 34xrred 41087 . . . . . . . 8 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) ≠ -∞) → (𝐴𝑖) ∈ ℝ)
3619, 35syldan 582 . . . . . . 7 (((𝜑𝑖𝑋) ∧ ¬ (𝐴𝑖) = -∞) → (𝐴𝑖) ∈ ℝ)
3717, 36eqeltrd 2860 . . . . . 6 (((𝜑𝑖𝑋) ∧ ¬ (𝐴𝑖) = -∞) → if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)) ∈ ℝ)
3815, 37pm2.61dan 800 . . . . 5 ((𝜑𝑖𝑋) → if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)) ∈ ℝ)
39 ioorrnopnxrlem.l . . . . 5 𝐿 = (𝑖𝑋 ↦ if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)))
4038, 39fmptd 6699 . . . 4 (𝜑𝐿:𝑋⟶ℝ)
41 iftrue 4350 . . . . . . . 8 ((𝐵𝑖) = +∞ → if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)) = ((𝐹𝑖) + 1))
4241adantl 474 . . . . . . 7 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)) = ((𝐹𝑖) + 1))
4311, 12readdcld 10467 . . . . . . . 8 ((𝜑𝑖𝑋) → ((𝐹𝑖) + 1) ∈ ℝ)
4443adantr 473 . . . . . . 7 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → ((𝐹𝑖) + 1) ∈ ℝ)
4542, 44eqeltrd 2860 . . . . . 6 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)) ∈ ℝ)
46 iffalse 4353 . . . . . . . 8 (¬ (𝐵𝑖) = +∞ → if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)) = (𝐵𝑖))
4746adantl 474 . . . . . . 7 (((𝜑𝑖𝑋) ∧ ¬ (𝐵𝑖) = +∞) → if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)) = (𝐵𝑖))
48 neqne 2969 . . . . . . . . 9 (¬ (𝐵𝑖) = +∞ → (𝐵𝑖) ≠ +∞)
4948adantl 474 . . . . . . . 8 (((𝜑𝑖𝑋) ∧ ¬ (𝐵𝑖) = +∞) → (𝐵𝑖) ≠ +∞)
5028adantr 473 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) ≠ +∞) → (𝐵𝑖) ∈ ℝ*)
51 mnfxr 10496 . . . . . . . . . . . 12 -∞ ∈ ℝ*
5251a1i 11 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → -∞ ∈ ℝ*)
5311mnfltd 12334 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → -∞ < (𝐹𝑖))
54 iooltub 41242 . . . . . . . . . . . . 13 (((𝐴𝑖) ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝐹𝑖) ∈ ((𝐴𝑖)(,)(𝐵𝑖))) → (𝐹𝑖) < (𝐵𝑖))
5521, 28, 10, 54syl3anc 1351 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (𝐹𝑖) < (𝐵𝑖))
5652, 26, 28, 53, 55xrlttrd 12367 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → -∞ < (𝐵𝑖))
5752, 28, 56xrgtned 41044 . . . . . . . . . 10 ((𝜑𝑖𝑋) → (𝐵𝑖) ≠ -∞)
5857adantr 473 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) ≠ +∞) → (𝐵𝑖) ≠ -∞)
59 simpr 477 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) ≠ +∞) → (𝐵𝑖) ≠ +∞)
6050, 58, 59xrred 41087 . . . . . . . 8 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) ≠ +∞) → (𝐵𝑖) ∈ ℝ)
6149, 60syldan 582 . . . . . . 7 (((𝜑𝑖𝑋) ∧ ¬ (𝐵𝑖) = +∞) → (𝐵𝑖) ∈ ℝ)
6247, 61eqeltrd 2860 . . . . . 6 (((𝜑𝑖𝑋) ∧ ¬ (𝐵𝑖) = +∞) → if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)) ∈ ℝ)
6345, 62pm2.61dan 800 . . . . 5 ((𝜑𝑖𝑋) → if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)) ∈ ℝ)
64 ioorrnopnxrlem.r . . . . 5 𝑅 = (𝑖𝑋 ↦ if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)))
6563, 64fmptd 6699 . . . 4 (𝜑𝑅:𝑋⟶ℝ)
663, 40, 65ioorrnopn 42046 . . 3 (𝜑X𝑖𝑋 ((𝐿𝑖)(,)(𝑅𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋)))
672, 66eqeltrd 2860 . 2 (𝜑𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)))
686elexd 3429 . . . . . 6 (𝜑𝐹 ∈ V)
69 ixpfn 8263 . . . . . . 7 (𝐹X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) → 𝐹 Fn 𝑋)
706, 69syl 17 . . . . . 6 (𝜑𝐹 Fn 𝑋)
7140ffvelrnda 6674 . . . . . . . . 9 ((𝜑𝑖𝑋) → (𝐿𝑖) ∈ ℝ)
7271rexrd 10488 . . . . . . . 8 ((𝜑𝑖𝑋) → (𝐿𝑖) ∈ ℝ*)
7365ffvelrnda 6674 . . . . . . . . 9 ((𝜑𝑖𝑋) → (𝑅𝑖) ∈ ℝ)
7473rexrd 10488 . . . . . . . 8 ((𝜑𝑖𝑋) → (𝑅𝑖) ∈ ℝ*)
7539a1i 11 . . . . . . . . . . . . 13 (𝜑𝐿 = (𝑖𝑋 ↦ if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖))))
7638elexd 3429 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)) ∈ V)
7775, 76fvmpt2d 6605 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (𝐿𝑖) = if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)))
7877adantr 473 . . . . . . . . . . 11 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → (𝐿𝑖) = if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)))
7978, 5eqtrd 2808 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → (𝐿𝑖) = ((𝐹𝑖) − 1))
8011ltm1d 11371 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐹𝑖) − 1) < (𝐹𝑖))
8180adantr 473 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → ((𝐹𝑖) − 1) < (𝐹𝑖))
8279, 81eqbrtrd 4947 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → (𝐿𝑖) < (𝐹𝑖))
8377adantr 473 . . . . . . . . . . 11 (((𝜑𝑖𝑋) ∧ ¬ (𝐴𝑖) = -∞) → (𝐿𝑖) = if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)))
8483, 17eqtrd 2808 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ ¬ (𝐴𝑖) = -∞) → (𝐿𝑖) = (𝐴𝑖))
8530adantr 473 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ ¬ (𝐴𝑖) = -∞) → (𝐴𝑖) < (𝐹𝑖))
8684, 85eqbrtrd 4947 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ ¬ (𝐴𝑖) = -∞) → (𝐿𝑖) < (𝐹𝑖))
8782, 86pm2.61dan 800 . . . . . . . 8 ((𝜑𝑖𝑋) → (𝐿𝑖) < (𝐹𝑖))
8811ltp1d 11369 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝐹𝑖) < ((𝐹𝑖) + 1))
8988adantr 473 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → (𝐹𝑖) < ((𝐹𝑖) + 1))
9064a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑅 = (𝑖𝑋 ↦ if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖))))
9163elexd 3429 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)) ∈ V)
9290, 91fvmpt2d 6605 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝑅𝑖) = if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)))
9392adantr 473 . . . . . . . . . . . 12 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → (𝑅𝑖) = if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)))
9493, 42eqtrd 2808 . . . . . . . . . . 11 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → (𝑅𝑖) = ((𝐹𝑖) + 1))
9594eqcomd 2778 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → ((𝐹𝑖) + 1) = (𝑅𝑖))
9689, 95breqtrd 4951 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → (𝐹𝑖) < (𝑅𝑖))
9755adantr 473 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ ¬ (𝐵𝑖) = +∞) → (𝐹𝑖) < (𝐵𝑖))
9892adantr 473 . . . . . . . . . . . 12 (((𝜑𝑖𝑋) ∧ ¬ (𝐵𝑖) = +∞) → (𝑅𝑖) = if((𝐵𝑖) = +∞, ((𝐹𝑖) + 1), (𝐵𝑖)))
9998, 47eqtrd 2808 . . . . . . . . . . 11 (((𝜑𝑖𝑋) ∧ ¬ (𝐵𝑖) = +∞) → (𝑅𝑖) = (𝐵𝑖))
10099eqcomd 2778 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ ¬ (𝐵𝑖) = +∞) → (𝐵𝑖) = (𝑅𝑖))
10197, 100breqtrd 4951 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ ¬ (𝐵𝑖) = +∞) → (𝐹𝑖) < (𝑅𝑖))
10296, 101pm2.61dan 800 . . . . . . . 8 ((𝜑𝑖𝑋) → (𝐹𝑖) < (𝑅𝑖))
10372, 74, 11, 87, 102eliood 41229 . . . . . . 7 ((𝜑𝑖𝑋) → (𝐹𝑖) ∈ ((𝐿𝑖)(,)(𝑅𝑖)))
104103ralrimiva 3126 . . . . . 6 (𝜑 → ∀𝑖𝑋 (𝐹𝑖) ∈ ((𝐿𝑖)(,)(𝑅𝑖)))
10568, 70, 1043jca 1108 . . . . 5 (𝜑 → (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑖𝑋 (𝐹𝑖) ∈ ((𝐿𝑖)(,)(𝑅𝑖))))
106 elixp2 8261 . . . . 5 (𝐹X𝑖𝑋 ((𝐿𝑖)(,)(𝑅𝑖)) ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑖𝑋 (𝐹𝑖) ∈ ((𝐿𝑖)(,)(𝑅𝑖))))
107105, 106sylibr 226 . . . 4 (𝜑𝐹X𝑖𝑋 ((𝐿𝑖)(,)(𝑅𝑖)))
108107, 1syl6eleqr 2871 . . 3 (𝜑𝐹𝑉)
10921adantr 473 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → (𝐴𝑖) ∈ ℝ*)
11072adantr 473 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → (𝐿𝑖) ∈ ℝ*)
11115mnfltd 12334 . . . . . . . . . . 11 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → -∞ < if((𝐴𝑖) = -∞, ((𝐹𝑖) − 1), (𝐴𝑖)))
112111, 5breqtrd 4951 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → -∞ < ((𝐹𝑖) − 1))
113 simpr 477 . . . . . . . . . . 11 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → (𝐴𝑖) = -∞)
114113, 79breq12d 4938 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → ((𝐴𝑖) < (𝐿𝑖) ↔ -∞ < ((𝐹𝑖) − 1)))
115112, 114mpbird 249 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → (𝐴𝑖) < (𝐿𝑖))
116109, 110, 115xrltled 12358 . . . . . . . 8 (((𝜑𝑖𝑋) ∧ (𝐴𝑖) = -∞) → (𝐴𝑖) ≤ (𝐿𝑖))
11784eqcomd 2778 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ ¬ (𝐴𝑖) = -∞) → (𝐴𝑖) = (𝐿𝑖))
11836, 117eqled 10541 . . . . . . . 8 (((𝜑𝑖𝑋) ∧ ¬ (𝐴𝑖) = -∞) → (𝐴𝑖) ≤ (𝐿𝑖))
119116, 118pm2.61dan 800 . . . . . . 7 ((𝜑𝑖𝑋) → (𝐴𝑖) ≤ (𝐿𝑖))
12074adantr 473 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → (𝑅𝑖) ∈ ℝ*)
12128adantr 473 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → (𝐵𝑖) ∈ ℝ*)
12244ltpnfd 12331 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → ((𝐹𝑖) + 1) < +∞)
123 simpr 477 . . . . . . . . . . 11 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → (𝐵𝑖) = +∞)
12494, 123breq12d 4938 . . . . . . . . . 10 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → ((𝑅𝑖) < (𝐵𝑖) ↔ ((𝐹𝑖) + 1) < +∞))
125122, 124mpbird 249 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → (𝑅𝑖) < (𝐵𝑖))
126120, 121, 125xrltled 12358 . . . . . . . 8 (((𝜑𝑖𝑋) ∧ (𝐵𝑖) = +∞) → (𝑅𝑖) ≤ (𝐵𝑖))
12773adantr 473 . . . . . . . . 9 (((𝜑𝑖𝑋) ∧ ¬ (𝐵𝑖) = +∞) → (𝑅𝑖) ∈ ℝ)
128127, 99eqled 10541 . . . . . . . 8 (((𝜑𝑖𝑋) ∧ ¬ (𝐵𝑖) = +∞) → (𝑅𝑖) ≤ (𝐵𝑖))
129126, 128pm2.61dan 800 . . . . . . 7 ((𝜑𝑖𝑋) → (𝑅𝑖) ≤ (𝐵𝑖))
130 ioossioo 12643 . . . . . . 7 ((((𝐴𝑖) ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ*) ∧ ((𝐴𝑖) ≤ (𝐿𝑖) ∧ (𝑅𝑖) ≤ (𝐵𝑖))) → ((𝐿𝑖)(,)(𝑅𝑖)) ⊆ ((𝐴𝑖)(,)(𝐵𝑖)))
13121, 28, 119, 129, 130syl22anc 826 . . . . . 6 ((𝜑𝑖𝑋) → ((𝐿𝑖)(,)(𝑅𝑖)) ⊆ ((𝐴𝑖)(,)(𝐵𝑖)))
132131ralrimiva 3126 . . . . 5 (𝜑 → ∀𝑖𝑋 ((𝐿𝑖)(,)(𝑅𝑖)) ⊆ ((𝐴𝑖)(,)(𝐵𝑖)))
133 ss2ixp 8270 . . . . 5 (∀𝑖𝑋 ((𝐿𝑖)(,)(𝑅𝑖)) ⊆ ((𝐴𝑖)(,)(𝐵𝑖)) → X𝑖𝑋 ((𝐿𝑖)(,)(𝑅𝑖)) ⊆ X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
134132, 133syl 17 . . . 4 (𝜑X𝑖𝑋 ((𝐿𝑖)(,)(𝑅𝑖)) ⊆ X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
1352, 134eqsstrd 3889 . . 3 (𝜑𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))
136108, 135jca 504 . 2 (𝜑 → (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
137 eleq2 2848 . . . 4 (𝑣 = 𝑉 → (𝐹𝑣𝐹𝑉))
138 sseq1 3876 . . . 4 (𝑣 = 𝑉 → (𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)) ↔ 𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
139137, 138anbi12d 621 . . 3 (𝑣 = 𝑉 → ((𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))) ↔ (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))))
140139rspcev 3529 . 2 ((𝑉 ∈ (TopOpen‘(ℝ^‘𝑋)) ∧ (𝐹𝑉𝑉X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖)))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
14167, 136, 140syl2anc 576 1 (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹𝑣𝑣X𝑖𝑋 ((𝐴𝑖)(,)(𝐵𝑖))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 387  w3a 1068   = wceq 1507  wcel 2050  wne 2961  wral 3082  wrex 3083  Vcvv 3409  wss 3823  ifcif 4344   class class class wbr 4925  cmpt 5004   Fn wfn 6180  wf 6181  cfv 6185  (class class class)co 6974  Xcixp 8257  Fincfn 8304  cr 10332  1c1 10334   + caddc 10336  +∞cpnf 10469  -∞cmnf 10470  *cxr 10471   < clt 10472  cle 10473  cmin 10668  (,)cioo 12552  TopOpenctopn 16549  ℝ^crrx 23701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5045  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277  ax-inf2 8896  ax-cnex 10389  ax-resscn 10390  ax-1cn 10391  ax-icn 10392  ax-addcl 10393  ax-addrcl 10394  ax-mulcl 10395  ax-mulrcl 10396  ax-mulcom 10397  ax-addass 10398  ax-mulass 10399  ax-distr 10400  ax-i2m1 10401  ax-1ne0 10402  ax-1rid 10403  ax-rnegex 10404  ax-rrecex 10405  ax-cnre 10406  ax-pre-lttri 10407  ax-pre-lttrn 10408  ax-pre-ltadd 10409  ax-pre-mulgt0 10410  ax-pre-sup 10411  ax-addf 10412  ax-mulf 10413
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-pss 3839  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-int 4746  df-iun 4790  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-se 5363  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-isom 6194  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-of 7225  df-om 7395  df-1st 7499  df-2nd 7500  df-supp 7632  df-tpos 7693  df-wrecs 7748  df-recs 7810  df-rdg 7848  df-1o 7903  df-oadd 7907  df-er 8087  df-map 8206  df-ixp 8258  df-en 8305  df-dom 8306  df-sdom 8307  df-fin 8308  df-fsupp 8627  df-sup 8699  df-inf 8700  df-oi 8767  df-card 9160  df-pnf 10474  df-mnf 10475  df-xr 10476  df-ltxr 10477  df-le 10478  df-sub 10670  df-neg 10671  df-div 11097  df-nn 11438  df-2 11501  df-3 11502  df-4 11503  df-5 11504  df-6 11505  df-7 11506  df-8 11507  df-9 11508  df-n0 11706  df-z 11792  df-dec 11910  df-uz 12057  df-q 12161  df-rp 12203  df-xneg 12322  df-xadd 12323  df-xmul 12324  df-ioo 12556  df-ico 12558  df-fz 12707  df-fzo 12848  df-seq 13183  df-exp 13243  df-hash 13504  df-cj 14317  df-re 14318  df-im 14319  df-sqrt 14453  df-abs 14454  df-clim 14704  df-sum 14902  df-struct 16339  df-ndx 16340  df-slot 16341  df-base 16343  df-sets 16344  df-ress 16345  df-plusg 16432  df-mulr 16433  df-starv 16434  df-sca 16435  df-vsca 16436  df-ip 16437  df-tset 16438  df-ple 16439  df-ds 16441  df-unif 16442  df-hom 16443  df-cco 16444  df-rest 16550  df-topn 16551  df-0g 16569  df-gsum 16570  df-topgen 16571  df-prds 16575  df-pws 16577  df-mgm 17722  df-sgrp 17764  df-mnd 17775  df-mhm 17815  df-submnd 17816  df-grp 17906  df-minusg 17907  df-sbg 17908  df-subg 18072  df-ghm 18139  df-cntz 18230  df-cmn 18680  df-abl 18681  df-mgp 18975  df-ur 18987  df-ring 19034  df-cring 19035  df-oppr 19108  df-dvdsr 19126  df-unit 19127  df-invr 19157  df-dvr 19168  df-rnghom 19202  df-drng 19239  df-field 19240  df-subrg 19268  df-abv 19322  df-staf 19350  df-srng 19351  df-lmod 19370  df-lss 19438  df-lmhm 19528  df-lvec 19609  df-sra 19678  df-rgmod 19679  df-psmet 20251  df-xmet 20252  df-met 20253  df-bl 20254  df-mopn 20255  df-cnfld 20260  df-refld 20463  df-phl 20484  df-dsmm 20590  df-frlm 20605  df-top 21218  df-topon 21235  df-topsp 21257  df-bases 21270  df-xms 22645  df-ms 22646  df-nm 22907  df-ngp 22908  df-tng 22909  df-nrg 22910  df-nlm 22911  df-clm 23382  df-cph 23487  df-tcph 23488  df-rrx 23703
This theorem is referenced by:  ioorrnopnxr  42048
  Copyright terms: Public domain W3C validator