Metamath Proof Explorer

Theorem ioorrnopnxrlem

Description: Given a point F that belongs to an indexed product of (possibly unbounded) open intervals, then F 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)

Ref Expression
Hypotheses ioorrnopnxrlem.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
ioorrnopnxrlem.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ* )
ioorrnopnxrlem.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ* )
ioorrnopnxrlem.f ⊢ ( 𝜑 → 𝐹 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
ioorrnopnxrlem.l ⊢ 𝐿 = ( 𝑖 ∈ 𝑋 ↦ if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) )
ioorrnopnxrlem.r ⊢ 𝑅 = ( 𝑖 ∈ 𝑋 ↦ if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) )
ioorrnopnxrlem.v ⊢ 𝑉 = X 𝑖 ∈ 𝑋 ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) )
Assertion ioorrnopnxrlem ( 𝜑 → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )

Proof

Step Hyp Ref Expression
1 ioorrnopnxrlem.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ioorrnopnxrlem.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ* )
3 ioorrnopnxrlem.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ* )
4 ioorrnopnxrlem.f ⊢ ( 𝜑 → 𝐹 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
5 ioorrnopnxrlem.l ⊢ 𝐿 = ( 𝑖 ∈ 𝑋 ↦ if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) )
6 ioorrnopnxrlem.r ⊢ 𝑅 = ( 𝑖 ∈ 𝑋 ↦ if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) )
7 ioorrnopnxrlem.v ⊢ 𝑉 = X 𝑖 ∈ 𝑋 ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) )
8 7 a1i ⊢ ( 𝜑 → 𝑉 = X 𝑖 ∈ 𝑋 ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) )
9 iftrue ⊢ ( ( 𝐴 ‘ 𝑖 ) = -∞ → if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝐹 ‘ 𝑖 ) − 1 ) )
10 9 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝐹 ‘ 𝑖 ) − 1 ) )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝐹 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
13 fvixp2 ⊢ ( ( 𝐹 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
14 11 12 13 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
15 14 elioored ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ )
16 1red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 1 ∈ ℝ )
17 15 16 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − 1 ) ∈ ℝ )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( ( 𝐹 ‘ 𝑖 ) − 1 ) ∈ ℝ )
19 10 18 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ )
20 iffalse ⊢ ( ¬ ( 𝐴 ‘ 𝑖 ) = -∞ → if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) = ( 𝐴 ‘ 𝑖 ) )
21 20 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑖 ) = -∞ ) → if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) = ( 𝐴 ‘ 𝑖 ) )
22 neqne ⊢ ( ¬ ( 𝐴 ‘ 𝑖 ) = -∞ → ( 𝐴 ‘ 𝑖 ) ≠ -∞ )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐴 ‘ 𝑖 ) ≠ -∞ )
24 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) ≠ -∞ ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
26 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) ≠ -∞ ) → ( 𝐴 ‘ 𝑖 ) ≠ -∞ )
27 pnfxr ⊢ +∞ ∈ ℝ*
28 27 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → +∞ ∈ ℝ* )
29 15 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ* )
30 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ* )
31 ioogtlb ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → ( 𝐴 ‘ 𝑖 ) < ( 𝐹 ‘ 𝑖 ) )
32 24 30 14 31 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) < ( 𝐹 ‘ 𝑖 ) )
33 15 ltpnfd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) < +∞ )
34 24 29 28 32 33 xrlttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) < +∞ )
35 24 28 34 xrltned ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ≠ +∞ )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) ≠ -∞ ) → ( 𝐴 ‘ 𝑖 ) ≠ +∞ )
37 25 26 36 xrred ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) ≠ -∞ ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
38 23 37 syldan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
39 21 38 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑖 ) = -∞ ) → if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ )
40 19 39 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ )
41 40 5 fmptd ⊢ ( 𝜑 → 𝐿 : 𝑋 ⟶ ℝ )
42 iftrue ⊢ ( ( 𝐵 ‘ 𝑖 ) = +∞ → if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) = ( ( 𝐹 ‘ 𝑖 ) + 1 ) )
43 42 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) = ( ( 𝐹 ‘ 𝑖 ) + 1 ) )
44 15 16 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) + 1 ) ∈ ℝ )
45 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( ( 𝐹 ‘ 𝑖 ) + 1 ) ∈ ℝ )
46 43 45 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
47 iffalse ⊢ ( ¬ ( 𝐵 ‘ 𝑖 ) = +∞ → if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) )
48 47 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐵 ‘ 𝑖 ) = +∞ ) → if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) )
49 neqne ⊢ ( ¬ ( 𝐵 ‘ 𝑖 ) = +∞ → ( 𝐵 ‘ 𝑖 ) ≠ +∞ )
50 49 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝐵 ‘ 𝑖 ) ≠ +∞ )
51 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) ≠ +∞ ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ* )
52 mnfxr ⊢ -∞ ∈ ℝ*
53 52 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → -∞ ∈ ℝ* )
54 15 mnfltd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → -∞ < ( 𝐹 ‘ 𝑖 ) )
55 iooltub ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) → ( 𝐹 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
56 24 30 14 55 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
57 53 29 30 54 56 xrlttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → -∞ < ( 𝐵 ‘ 𝑖 ) )
58 53 30 57 xrgtned ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ≠ -∞ )
59 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) ≠ +∞ ) → ( 𝐵 ‘ 𝑖 ) ≠ -∞ )
60 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) ≠ +∞ ) → ( 𝐵 ‘ 𝑖 ) ≠ +∞ )
61 51 59 60 xrred ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) ≠ +∞ ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
62 50 61 syldan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
63 48 62 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐵 ‘ 𝑖 ) = +∞ ) → if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
64 46 63 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
65 64 6 fmptd ⊢ ( 𝜑 → 𝑅 : 𝑋 ⟶ ℝ )
66 1 41 65 ioorrnopn ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
67 8 66 eqeltrd ⊢ ( 𝜑 → 𝑉 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
68 4 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
69 ixpfn ⊢ ( 𝐹 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) → 𝐹 Fn 𝑋 )
70 4 69 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
71 41 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐿 ‘ 𝑖 ) ∈ ℝ )
72 71 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐿 ‘ 𝑖 ) ∈ ℝ* )
73 65 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑅 ‘ 𝑖 ) ∈ ℝ )
74 73 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑅 ‘ 𝑖 ) ∈ ℝ* )
75 5 a1i ⊢ ( 𝜑 → 𝐿 = ( 𝑖 ∈ 𝑋 ↦ if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) ) )
76 40 elexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) ∈ V )
77 75 76 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐿 ‘ 𝑖 ) = if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) )
78 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐿 ‘ 𝑖 ) = if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) )
79 78 10 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐿 ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝑖 ) − 1 ) )
80 15 ltm1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑖 ) − 1 ) < ( 𝐹 ‘ 𝑖 ) )
81 80 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( ( 𝐹 ‘ 𝑖 ) − 1 ) < ( 𝐹 ‘ 𝑖 ) )
82 79 81 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐿 ‘ 𝑖 ) < ( 𝐹 ‘ 𝑖 ) )
83 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐿 ‘ 𝑖 ) = if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) )
84 83 21 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐿 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
85 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐴 ‘ 𝑖 ) < ( 𝐹 ‘ 𝑖 ) )
86 84 85 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐿 ‘ 𝑖 ) < ( 𝐹 ‘ 𝑖 ) )
87 82 86 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐿 ‘ 𝑖 ) < ( 𝐹 ‘ 𝑖 ) )
88 15 ltp1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) < ( ( 𝐹 ‘ 𝑖 ) + 1 ) )
89 88 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝐹 ‘ 𝑖 ) < ( ( 𝐹 ‘ 𝑖 ) + 1 ) )
90 6 a1i ⊢ ( 𝜑 → 𝑅 = ( 𝑖 ∈ 𝑋 ↦ if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) ) )
91 64 elexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) ∈ V )
92 90 91 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑅 ‘ 𝑖 ) = if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) )
93 92 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝑅 ‘ 𝑖 ) = if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) )
94 93 43 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝑅 ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝑖 ) + 1 ) )
95 94 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( ( 𝐹 ‘ 𝑖 ) + 1 ) = ( 𝑅 ‘ 𝑖 ) )
96 89 95 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝐹 ‘ 𝑖 ) < ( 𝑅 ‘ 𝑖 ) )
97 56 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝐹 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
98 92 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝑅 ‘ 𝑖 ) = if ( ( 𝐵 ‘ 𝑖 ) = +∞ , ( ( 𝐹 ‘ 𝑖 ) + 1 ) , ( 𝐵 ‘ 𝑖 ) ) )
99 98 48 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝑅 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) )
100 99 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝐵 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) )
101 97 100 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝐹 ‘ 𝑖 ) < ( 𝑅 ‘ 𝑖 ) )
102 96 101 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) < ( 𝑅 ‘ 𝑖 ) )
103 72 74 15 87 102 eliood ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) )
104 103 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑋 ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) )
105 68 70 104 3jca ⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) ) )
106 elixp2 ⊢ ( 𝐹 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝐹 ‘ 𝑖 ) ∈ ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) ) )
107 105 106 sylibr ⊢ ( 𝜑 → 𝐹 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) )
108 107 7 eleqtrrdi ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
109 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
110 72 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐿 ‘ 𝑖 ) ∈ ℝ* )
111 19 mnfltd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → -∞ < if ( ( 𝐴 ‘ 𝑖 ) = -∞ , ( ( 𝐹 ‘ 𝑖 ) − 1 ) , ( 𝐴 ‘ 𝑖 ) ) )
112 111 10 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → -∞ < ( ( 𝐹 ‘ 𝑖 ) − 1 ) )
113 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐴 ‘ 𝑖 ) = -∞ )
114 113 79 breq12d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( ( 𝐴 ‘ 𝑖 ) < ( 𝐿 ‘ 𝑖 ) ↔ -∞ < ( ( 𝐹 ‘ 𝑖 ) − 1 ) ) )
115 112 114 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐴 ‘ 𝑖 ) < ( 𝐿 ‘ 𝑖 ) )
116 109 110 115 xrltled ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐴 ‘ 𝑖 ) ≤ ( 𝐿 ‘ 𝑖 ) )
117 84 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐴 ‘ 𝑖 ) = ( 𝐿 ‘ 𝑖 ) )
118 38 117 eqled ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐴 ‘ 𝑖 ) = -∞ ) → ( 𝐴 ‘ 𝑖 ) ≤ ( 𝐿 ‘ 𝑖 ) )
119 116 118 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ≤ ( 𝐿 ‘ 𝑖 ) )
120 74 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝑅 ‘ 𝑖 ) ∈ ℝ* )
121 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ* )
122 45 ltpnfd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( ( 𝐹 ‘ 𝑖 ) + 1 ) < +∞ )
123 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝐵 ‘ 𝑖 ) = +∞ )
124 94 123 breq12d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( ( 𝑅 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) ↔ ( ( 𝐹 ‘ 𝑖 ) + 1 ) < +∞ ) )
125 122 124 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝑅 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
126 120 121 125 xrltled ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝑅 ‘ 𝑖 ) ≤ ( 𝐵 ‘ 𝑖 ) )
127 73 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝑅 ‘ 𝑖 ) ∈ ℝ )
128 127 99 eqled ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ ¬ ( 𝐵 ‘ 𝑖 ) = +∞ ) → ( 𝑅 ‘ 𝑖 ) ≤ ( 𝐵 ‘ 𝑖 ) )
129 126 128 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑅 ‘ 𝑖 ) ≤ ( 𝐵 ‘ 𝑖 ) )
130 ioossioo ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℝ* ) ∧ ( ( 𝐴 ‘ 𝑖 ) ≤ ( 𝐿 ‘ 𝑖 ) ∧ ( 𝑅 ‘ 𝑖 ) ≤ ( 𝐵 ‘ 𝑖 ) ) ) → ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) ⊆ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
131 24 30 119 129 130 syl22anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) ⊆ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
132 131 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑋 ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) ⊆ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
133 ss2ixp ⊢ ( ∀ 𝑖 ∈ 𝑋 ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) ⊆ ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) → X 𝑖 ∈ 𝑋 ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
134 132 133 syl ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐿 ‘ 𝑖 ) (,) ( 𝑅 ‘ 𝑖 ) ) ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
135 8 134 eqsstrd ⊢ ( 𝜑 → 𝑉 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) )
136 108 135 jca ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
137 eleq2 ⊢ ( 𝑣 = 𝑉 → ( 𝐹 ∈ 𝑣 ↔ 𝐹 ∈ 𝑉 ) )
138 sseq1 ⊢ ( 𝑣 = 𝑉 → ( 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ↔ 𝑉 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
139 137 138 anbi12d ⊢ ( 𝑣 = 𝑉 → ( ( 𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ↔ ( 𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ) )
140 139 rspcev ⊢ ( ( 𝑉 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )
141 67 136 140 syl2anc ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ( 𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ) )