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 birani ⊢ ( ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ∀ 𝑖 ∈ 𝑋 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
147 simpr ⊢ ( ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
148 rspa ⊢ ( ( ∀ 𝑖 ∈ 𝑋 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
149 146 147 148 syl2anc ⊢ ( ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
150 149 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
151 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
152 71 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
153 85 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ* )
154 simpll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝜑 )
155 eldifi ⊢ ( 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) )
156 155 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) )
157 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
158 ioossre ⊢ ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) ⊆ ℝ
159 simplr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) )
160 65 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
161 159 160 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
162 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
163 15 fvixp ⊢ ( ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) )
164 161 162 163 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) )
165 158 164 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
166 154 156 157 165 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
167 166 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ* )
168 simpl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → 𝜑 )
169 155 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) )
170 168 169 jca ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) )
171 170 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) )
172 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → 𝑖 ∈ 𝑋 )
173 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) )
174 ixpfn ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) → 𝑓 Fn 𝑋 )
175 161 174 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 Fn 𝑋 )
176 175 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → 𝑓 Fn 𝑋 )
177 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑖 ) )
178 177 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑖 ) )
179 23 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → -∞ ∈ ℝ* )
180 71 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ* )
181 165 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
182 181 mnfltd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → -∞ < ( 𝑓 ‘ 𝑖 ) )
183 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) )
184 179 180 181 182 183 eliood ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) )
185 184 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) )
186 178 185 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) )
187 186 adantlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) )
188 78 eqcomd ⊢ ( 𝑘 = 𝑖 → ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) = if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
189 188 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝑖 ) → ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) = if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
190 187 189 eleqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
191 15 158 eqsstrdi ⊢ ( 𝑘 = 𝑖 → if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ⊆ ℝ )
192 ssid ⊢ ℝ ⊆ ℝ
193 20 192 eqsstrdi ⊢ ( ¬ 𝑘 = 𝑖 → if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ⊆ ℝ )
194 191 193 pm2.61i ⊢ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ⊆ ℝ
195 161 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
196 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
197 fvixp2 ⊢ ( ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
198 195 196 197 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) , ℝ ) )
199 194 198 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
200 199 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ )
201 iffalse ⊢ ( ¬ 𝑘 = 𝑖 → if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) = ℝ )
202 201 eqcomd ⊢ ( ¬ 𝑘 = 𝑖 → ℝ = if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
203 202 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝑖 ) → ℝ = if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
204 200 203 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
205 204 adantllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) ∧ ¬ 𝑘 = 𝑖 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
206 190 205 pm2.61dan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
207 206 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
208 176 207 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) ) )
209 51 elixp ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) ↔ ( 𝑓 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑓 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) ) )
210 208 209 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) )
211 74 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) = ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
212 211 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) ( 𝐴 ‘ 𝑖 ) ) , ℝ ) = ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
213 210 212 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
214 171 172 173 213 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
215 eldifn ⊢ ( 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → ¬ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
216 215 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) → ¬ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) )
217 214 216 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ¬ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) )
218 154 157 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
219 218 166 lenltd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑖 ) ≤ ( 𝑓 ‘ 𝑖 ) ↔ ¬ ( 𝑓 ‘ 𝑖 ) < ( 𝐴 ‘ 𝑖 ) ) )
220 217 219 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ≤ ( 𝑓 ‘ 𝑖 ) )
221 23 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → -∞ ∈ ℝ* )
222 85 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ* )
223 iooltub ⊢ ( ( -∞ ∈ ℝ* ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑓 ‘ 𝑖 ) ∈ ( -∞ (,) ( 𝐵 ‘ 𝑖 ) ) ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
224 221 222 164 223 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
225 154 156 157 224 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) < ( 𝐵 ‘ 𝑖 ) )
226 152 153 167 220 225 elicod ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
227 145 150 151 226 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
228 227 ex ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → ( 𝑖 ∈ 𝑋 → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) )
229 144 228 ralrimi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ 𝑋 ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
230 141 229 jca ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → ( 𝑓 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) )
231 230 87 sylibr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
232 231 ex ⊢ ( 𝜑 → ( 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) )
233 110 232 impbid ⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) )
234 233 alrimiv ⊢ ( 𝜑 → ∀ 𝑓 ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) )
235 dfcleq ⊢ ( X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ↔ ∀ 𝑓 ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) )
236 234 235 sylibr ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )