Metamath Proof Explorer

Theorem hspdifhsp

Description: A n-dimensional half-open interval is the intersection of the difference of half spaces. This is a substep of Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hspdifhsp.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hspdifhsp.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
hspdifhsp.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
hspdifhsp.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
hspdifhsp.h ⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
Assertion hspdifhsp ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )

Proof

Step Hyp Ref Expression
1 hspdifhsp.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 hspdifhsp.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3 hspdifhsp.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
4 hspdifhsp.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
5 hspdifhsp.h ⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
6 nfv ⊢ Ⅎ 𝑖 𝜑
7 nfcv ⊢ Ⅎ 𝑖 𝑓
8 nfixp1 ⊢ Ⅎ 𝑖 X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) )
9 7 8 nfel ⊢ Ⅎ 𝑖 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) )
10 6 9 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
11 ixpfn ⊢ ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) → 𝑓 Fn 𝑋 )
12 11 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 Fn 𝑋 )
13 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑖 ) )
14 13 oveq2d ⊢ ( 𝑘 = 𝑖 → ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) = ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) )
15 iftrue ⊢ ( 𝑘 = 𝑖 → if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) = ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) )
16 14 15 eqtr4d ⊢ ( 𝑘 = 𝑖 → ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) = if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
17 eqimss ⊢ ( ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) = if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) → ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) ⊆ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
18 16 17 syl ⊢ ( 𝑘 = 𝑖 → ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) ⊆ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
19 ioossre ⊢ ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ℝ
20 iffalse ⊢ ( ¬ 𝑘 = 𝑖 → if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) = ℝ )
21 19 20 sseqtrrid ⊢ ( ¬ 𝑘 = 𝑖 → ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) ⊆ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
22 18 21 pm2.61i ⊢ ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) ⊆ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ )
23 mnfxr ⊢ -∞ ∈ ℝ*
24 23 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → -∞ ∈ ℝ* )
25 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
26 25 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
27 26 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
28 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
29 icossre ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ* ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ℝ )
30 28 26 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ℝ )
31 30 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ℝ )
32 simpl ⊢ ( ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
33 simpr ⊢ ( ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
34 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑘 ) )
35 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑘 ) )
36 34 35 oveq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
37 36 fvixp ⊢ ( ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
38 32 33 37 syl2anc ⊢ ( ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
39 38 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
40 31 39 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
41 40 mnfltd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → -∞ < ( 𝑓 ‘ 𝑘 ) )
42 28 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ* )
43 42 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ* )
44 icoltub ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ* ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) → ( 𝑓 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
45 43 27 39 44 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) )
46 24 27 40 41 45 eliood ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) )
47 22 46 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
48 47 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
49 48 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
50 12 49 jca ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ) )
51 vex ⊢ 𝑓 ∈ V
52 51 elixp ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ↔ ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ) )
53 50 52 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
54 equequ1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 = 𝑙 ↔ 𝑘 = 𝑙 ) )
55 54 ifbid ⊢ ( 𝑖 = 𝑘 → if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) = if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) )
56 55 cbvixpv ⊢ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) = X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ )
57 56 a1i ⊢ ( ( 𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ ) → X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) = X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) )
58 57 mpoeq3ia ⊢ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) = ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) )
59 58 mpteq2i ⊢ ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) ) = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
60 5 59 eqtri ⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
61 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝑋 ∈ Fin )
62 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
63 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝐵 : 𝑋 ⟶ ℝ )
64 63 62 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
65 60 61 62 64 hspval ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
66 65 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
67 53 66 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) )
68 23 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → -∞ ∈ ℝ* )
69 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝐴 : 𝑋 ⟶ ℝ )
70 69 62 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
71 70 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
72 71 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
73 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
74 60 61 62 70 hspval ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
75 74 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
76 73 75 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
77 62 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → 𝑖 ∈ 𝑋 )
78 iftrue ⊢ ( 𝑘 = 𝑖 → if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) = ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) )
79 78 fvixp ⊢ ( ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) )
80 76 77 79 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) )
81 iooltub ⊢ ( ( -∞ ∈ ℝ* ∧ ( 𝐴 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) )
82 68 72 80 81 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) )
83 82 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) )
84 71 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
85 64 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ* )
86 85 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ* )
87 51 elixp ⊢ ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ↔ ( 𝑓 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) )
88 87 biimpi ⊢ ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) )
89 88 simprd ⊢ ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) → ∀ 𝑖 ∈ 𝑋 ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
90 rspa ⊢ ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
91 89 90 sylan ⊢ ( ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
92 91 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
93 icogelb ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) → ( 𝐴 ‘ 𝑖 ) ≤ ( 𝑓 ‘ 𝑖 ) )
94 84 86 92 93 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ≤ ( 𝑓 ‘ 𝑖 ) )
95 70 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
96 icossre ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℝ* ) → ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ℝ )
97 70 85 96 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ℝ )
98 97 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ℝ )
99 98 92 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
100 95 99 lenltd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑖 ) ≤ ( 𝑓 ‘ 𝑖 ) ↔ ¬ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) )
101 94 100 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ¬ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) )
102 101 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → ¬ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) )
103 83 102 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ¬ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
104 67 103 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
105 104 ex ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) → ( 𝑖 ∈ 𝑋 → 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) )
106 10 105 ralrimi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ 𝑋 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
107 eliin ⊢ ( 𝑓 ∈ V → ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ 𝑋 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) )
108 51 107 ax-mp ⊢ ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ 𝑋 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
109 106 108 sylibr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
110 109 ex ⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) )
111 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑘 𝑘 ∈ 𝑋 )
112 111 biimpi ⊢ ( 𝑋 ≠ ∅ → ∃ 𝑘 𝑘 ∈ 𝑋 )
113 2 112 syl ⊢ ( 𝜑 → ∃ 𝑘 𝑘 ∈ 𝑋 )
114 113 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → ∃ 𝑘 𝑘 ∈ 𝑋 )
115 simpl ⊢ ( ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
116 simpr ⊢ ( ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
117 id ⊢ ( 𝑖 = 𝑘 → 𝑖 = 𝑘 )
118 117 35 oveq12d ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) = ( 𝑘 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑘 ) ) )
119 117 34 oveq12d ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) = ( 𝑘 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑘 ) ) )
120 118 119 difeq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) = ( ( 𝑘 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑘 ) ) ∖ ( 𝑘 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑘 ) ) ) )
121 120 eleq2d ⊢ ( 𝑖 = 𝑘 → ( 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ↔ 𝑓 ∈ ( ( 𝑘 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑘 ) ) ∖ ( 𝑘 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑘 ) ) ) ) )
122 115 116 121 eliind ⊢ ( ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑓 ∈ ( ( 𝑘 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑘 ) ) ∖ ( 𝑘 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑘 ) ) ) )
123 122 eldifad ⊢ ( ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑓 ∈ ( 𝑘 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑘 ) ) )
124 123 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑓 ∈ ( 𝑘 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑘 ) ) )
125 equequ1 ⊢ ( 𝑖 = ℎ → ( 𝑖 = 𝑙 ↔ ℎ = 𝑙 ) )
126 125 ifbid ⊢ ( 𝑖 = ℎ → if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) = if ( ℎ = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) )
127 126 cbvixpv ⊢ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) = X ℎ ∈ 𝑥 if ( ℎ = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ )
128 127 a1i ⊢ ( ( 𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ ) → X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) = X ℎ ∈ 𝑥 if ( ℎ = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) )
129 128 mpoeq3ia ⊢ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) = ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X ℎ ∈ 𝑥 if ( ℎ = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) )
130 129 mpteq2i ⊢ ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) ) = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X ℎ ∈ 𝑥 if ( ℎ = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
131 5 130 eqtri ⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X ℎ ∈ 𝑥 if ( ℎ = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
132 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑋 ∈ Fin )
133 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
134 25 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
135 131 132 133 134 hspval ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑘 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑘 ) ) = X ℎ ∈ 𝑋 if ( ℎ = 𝑘 , ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) , ℝ ) )
136 124 135 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑓 ∈ X ℎ ∈ 𝑋 if ( ℎ = 𝑘 , ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) , ℝ ) )
137 ixpfn ⊢ ( 𝑓 ∈ X ℎ ∈ 𝑋 if ( ℎ = 𝑘 , ( -∞ (,) ( 𝐵 ‘ 𝑘 ) ) , ℝ ) → 𝑓 Fn 𝑋 )
138 136 137 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝑓 Fn 𝑋 )
139 138 ex ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → ( 𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋 ) )
140 139 exlimdv ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → ( ∃ 𝑘 𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋 ) )
141 114 140 mpd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → 𝑓 Fn 𝑋 )
142 nfii1 ⊢ Ⅎ 𝑖 ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
143 7 142 nfel ⊢ Ⅎ 𝑖 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
144 6 143 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
145 simpll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝜑 )
146 108 biimpi ⊢ ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ 𝑋 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
147 146 adantr ⊢ ( ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ∀ 𝑖 ∈ 𝑋 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
148 simpr ⊢ ( ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
149 rspa ⊢ ( ( ∀ 𝑖 ∈ 𝑋 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
150 147 148 149 syl2anc ⊢ ( ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
151 150 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
152 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
153 71 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
154 85 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ* )
155 simpll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝜑 )
156 eldifi ⊢ ( 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) )
157 156 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) )
158 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
159 ioossre ⊢ ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ℝ
160 simplr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) )
161 65 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
162 160 161 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
163 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
164 15 fvixp ⊢ ( ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) )
165 162 163 164 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) )
166 159 165 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
167 155 157 158 166 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
168 167 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ* )
169 simpl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → 𝜑 )
170 156 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) )
171 169 170 jca ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) )
172 171 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) )
173 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → 𝑖 ∈ 𝑋 )
174 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) )
175 ixpfn ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) → 𝑓 Fn 𝑋 )
176 162 175 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 Fn 𝑋 )
177 176 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → 𝑓 Fn 𝑋 )
178 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑖 ) )
179 178 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑖 ) )
180 23 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → -∞ ∈ ℝ* )
181 71 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
182 166 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
183 182 mnfltd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → -∞ < ( 𝑓 ‘ 𝑖 ) )
184 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) )
185 180 181 182 183 184 eliood ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) )
186 185 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) )
187 179 186 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) )
188 187 adantlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) )
189 78 eqcomd ⊢ ( 𝑘 = 𝑖 → ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) = if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
190 189 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝑖 ) → ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) = if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
191 188 190 eleqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
192 15 159 eqsstrdi ⊢ ( 𝑘 = 𝑖 → if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ⊆ ℝ )
193 ssid ⊢ ℝ ⊆ ℝ
194 20 193 eqsstrdi ⊢ ( ¬ 𝑘 = 𝑖 → if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ⊆ ℝ )
195 192 194 pm2.61i ⊢ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ⊆ ℝ
196 162 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
197 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
198 fvixp2 ⊢ ( ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
199 196 197 198 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
200 195 199 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
201 200 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
202 iffalse ⊢ ( ¬ 𝑘 = 𝑖 → if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) = ℝ )
203 202 eqcomd ⊢ ( ¬ 𝑘 = 𝑖 → ℝ = if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
204 203 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝑖 ) → ℝ = if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
205 201 204 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
206 205 adantllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
207 191 206 pm2.61dan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
208 207 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
209 177 208 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) ) )
210 51 elixp ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) ↔ ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) ) )
211 209 210 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
212 74 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) = ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
213 212 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) = ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
214 211 213 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
215 172 173 174 214 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
216 eldifn ⊢ ( 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → ¬ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
217 216 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ¬ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
218 215 217 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ¬ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) )
219 155 158 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
220 219 167 lenltd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑖 ) ≤ ( 𝑓 ‘ 𝑖 ) ↔ ¬ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) )
221 218 220 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ≤ ( 𝑓 ‘ 𝑖 ) )
222 23 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → -∞ ∈ ℝ* )
223 85 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ* )
224 iooltub ⊢ ( ( -∞ ∈ ℝ* ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
225 222 223 165 224 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
226 155 157 158 225 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
227 153 154 168 221 226 elicod ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
228 145 151 152 227 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
229 228 ex ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → ( 𝑖 ∈ 𝑋 → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) )
230 144 229 ralrimi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ 𝑋 ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
231 141 230 jca ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) )
232 231 87 sylibr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
233 232 ex ⊢ ( 𝜑 → ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) )
234 110 233 impbid ⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) )
235 234 alrimiv ⊢ ( 𝜑 → ∀ 𝑓 ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) )
236 dfcleq ⊢ ( X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ↔ ∀ 𝑓 ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) )
237 235 236 sylibr ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )