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
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) |
26 |
25
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* ) |
27 |
26
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* ) |
28 |
3
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ ) |
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
|
sseldi |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 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
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ ) |
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
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ ) |
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
|
sseldi |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ ) |
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
|
sseldi |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℝ ) |
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 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ) |