Step | Hyp | Ref
| Expression |
1 | | ovolicc2.7 |
. . . 4
β’ (π β (π΄[,]π΅) β βͺ π) |
2 | | ovolicc.1 |
. . . . . 6
β’ (π β π΄ β β) |
3 | 2 | rexrd 11210 |
. . . . 5
β’ (π β π΄ β
β*) |
4 | | ovolicc.2 |
. . . . . 6
β’ (π β π΅ β β) |
5 | 4 | rexrd 11210 |
. . . . 5
β’ (π β π΅ β
β*) |
6 | | ovolicc.3 |
. . . . 5
β’ (π β π΄ β€ π΅) |
7 | | lbicc2 13387 |
. . . . 5
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΄ β (π΄[,]π΅)) |
8 | 3, 5, 6, 7 | syl3anc 1372 |
. . . 4
β’ (π β π΄ β (π΄[,]π΅)) |
9 | 1, 8 | sseldd 3946 |
. . 3
β’ (π β π΄ β βͺ π) |
10 | | eluni2 4870 |
. . 3
β’ (π΄ β βͺ π
β βπ§ β
π π΄ β π§) |
11 | 9, 10 | sylib 217 |
. 2
β’ (π β βπ§ β π π΄ β π§) |
12 | | ovolicc2.6 |
. . . . . . 7
β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) |
13 | 12 | elin2d 4160 |
. . . . . 6
β’ (π β π β Fin) |
14 | | ovolicc2.10 |
. . . . . . 7
β’ π = {π’ β π β£ (π’ β© (π΄[,]π΅)) β β
} |
15 | 14 | ssrab3 4041 |
. . . . . 6
β’ π β π |
16 | | ssfi 9120 |
. . . . . 6
β’ ((π β Fin β§ π β π) β π β Fin) |
17 | 13, 15, 16 | sylancl 587 |
. . . . 5
β’ (π β π β Fin) |
18 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (π΄[,]π΅) β βͺ π) |
19 | | ovolicc2.8 |
. . . . . . . . . . . . . . 15
β’ (π β πΊ:πβΆβ) |
20 | | ineq1 4166 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = π‘ β (π’ β© (π΄[,]π΅)) = (π‘ β© (π΄[,]π΅))) |
21 | 20 | neeq1d 3000 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π‘ β ((π’ β© (π΄[,]π΅)) β β
β (π‘ β© (π΄[,]π΅)) β β
)) |
22 | 21, 14 | elrab2 3649 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β π β (π‘ β π β§ (π‘ β© (π΄[,]π΅)) β β
)) |
23 | 22 | simplbi 499 |
. . . . . . . . . . . . . . 15
β’ (π‘ β π β π‘ β π) |
24 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . 15
β’ ((πΊ:πβΆβ β§ π‘ β π) β (πΊβπ‘) β β) |
25 | 19, 23, 24 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β π) β (πΊβπ‘) β β) |
26 | | ovolicc2.5 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
27 | 26 | ffvelcdmda 7036 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πΊβπ‘) β β) β (πΉβ(πΊβπ‘)) β ( β€ β© (β Γ
β))) |
28 | 25, 27 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β π) β (πΉβ(πΊβπ‘)) β ( β€ β© (β Γ
β))) |
29 | 28 | elin2d 4160 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β (πΉβ(πΊβπ‘)) β (β Γ
β)) |
30 | | xp2nd 7955 |
. . . . . . . . . . . 12
β’ ((πΉβ(πΊβπ‘)) β (β Γ β) β
(2nd β(πΉβ(πΊβπ‘))) β β) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β (2nd β(πΉβ(πΊβπ‘))) β β) |
32 | 4 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β π΅ β β) |
33 | 31, 32 | ifcld 4533 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β β) |
34 | 22 | simprbi 498 |
. . . . . . . . . . . . . 14
β’ (π‘ β π β (π‘ β© (π΄[,]π΅)) β β
) |
35 | 34 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β π) β (π‘ β© (π΄[,]π΅)) β β
) |
36 | | n0 4307 |
. . . . . . . . . . . . 13
β’ ((π‘ β© (π΄[,]π΅)) β β
β βπ¦ π¦ β (π‘ β© (π΄[,]π΅))) |
37 | 35, 36 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β βπ¦ π¦ β (π‘ β© (π΄[,]π΅))) |
38 | 2 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π΄ β β) |
39 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π¦ β (π‘ β© (π΄[,]π΅))) |
40 | 39 | elin2d 4160 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π¦ β (π΄[,]π΅)) |
41 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π΅ β β) |
42 | | elicc2 13335 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β β β§ π΅ β β) β (π¦ β (π΄[,]π΅) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅))) |
43 | 2, 41, 42 | syl2an2r 684 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β (π¦ β (π΄[,]π΅) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅))) |
44 | 40, 43 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅)) |
45 | 44 | simp1d 1143 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π¦ β β) |
46 | 29 | adantrr 716 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β (πΉβ(πΊβπ‘)) β (β Γ
β)) |
47 | 46, 30 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β (2nd β(πΉβ(πΊβπ‘))) β β) |
48 | 44 | simp2d 1144 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π΄ β€ π¦) |
49 | 39 | elin1d 4159 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π¦ β π‘) |
50 | 25 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β (πΊβπ‘) β β) |
51 | | fvco3 6941 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ (πΊβπ‘) β β) β (((,) β πΉ)β(πΊβπ‘)) = ((,)β(πΉβ(πΊβπ‘)))) |
52 | 26, 50, 51 | syl2an2r 684 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β (((,) β πΉ)β(πΊβπ‘)) = ((,)β(πΉβ(πΊβπ‘)))) |
53 | | ovolicc2.9 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) |
54 | 23, 53 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) |
55 | 54 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β (((,) β πΉ)β(πΊβπ‘)) = π‘) |
56 | | 1st2nd2 7961 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΉβ(πΊβπ‘)) β (β Γ β) β
(πΉβ(πΊβπ‘)) = β¨(1st β(πΉβ(πΊβπ‘))), (2nd β(πΉβ(πΊβπ‘)))β©) |
57 | 46, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β (πΉβ(πΊβπ‘)) = β¨(1st β(πΉβ(πΊβπ‘))), (2nd β(πΉβ(πΊβπ‘)))β©) |
58 | 57 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β ((,)β(πΉβ(πΊβπ‘))) = ((,)ββ¨(1st
β(πΉβ(πΊβπ‘))), (2nd β(πΉβ(πΊβπ‘)))β©)) |
59 | | df-ov 7361 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((1st β(πΉβ(πΊβπ‘)))(,)(2nd β(πΉβ(πΊβπ‘)))) = ((,)ββ¨(1st
β(πΉβ(πΊβπ‘))), (2nd β(πΉβ(πΊβπ‘)))β©) |
60 | 58, 59 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β ((,)β(πΉβ(πΊβπ‘))) = ((1st β(πΉβ(πΊβπ‘)))(,)(2nd β(πΉβ(πΊβπ‘))))) |
61 | 52, 55, 60 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π‘ = ((1st β(πΉβ(πΊβπ‘)))(,)(2nd β(πΉβ(πΊβπ‘))))) |
62 | 49, 61 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π¦ β ((1st β(πΉβ(πΊβπ‘)))(,)(2nd β(πΉβ(πΊβπ‘))))) |
63 | | xp1st 7954 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉβ(πΊβπ‘)) β (β Γ β) β
(1st β(πΉβ(πΊβπ‘))) β β) |
64 | 46, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β (1st β(πΉβ(πΊβπ‘))) β β) |
65 | | rexr 11206 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1st β(πΉβ(πΊβπ‘))) β β β (1st
β(πΉβ(πΊβπ‘))) β
β*) |
66 | | rexr 11206 |
. . . . . . . . . . . . . . . . . . . 20
β’
((2nd β(πΉβ(πΊβπ‘))) β β β (2nd
β(πΉβ(πΊβπ‘))) β
β*) |
67 | | elioo2 13311 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((1st β(πΉβ(πΊβπ‘))) β β* β§
(2nd β(πΉβ(πΊβπ‘))) β β*) β (π¦ β ((1st
β(πΉβ(πΊβπ‘)))(,)(2nd β(πΉβ(πΊβπ‘)))) β (π¦ β β β§ (1st
β(πΉβ(πΊβπ‘))) < π¦ β§ π¦ < (2nd β(πΉβ(πΊβπ‘)))))) |
68 | 65, 66, 67 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
β’
(((1st β(πΉβ(πΊβπ‘))) β β β§ (2nd
β(πΉβ(πΊβπ‘))) β β) β (π¦ β ((1st
β(πΉβ(πΊβπ‘)))(,)(2nd β(πΉβ(πΊβπ‘)))) β (π¦ β β β§ (1st
β(πΉβ(πΊβπ‘))) < π¦ β§ π¦ < (2nd β(πΉβ(πΊβπ‘)))))) |
69 | 64, 47, 68 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β (π¦ β ((1st β(πΉβ(πΊβπ‘)))(,)(2nd β(πΉβ(πΊβπ‘)))) β (π¦ β β β§ (1st
β(πΉβ(πΊβπ‘))) < π¦ β§ π¦ < (2nd β(πΉβ(πΊβπ‘)))))) |
70 | 62, 69 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β (π¦ β β β§ (1st
β(πΉβ(πΊβπ‘))) < π¦ β§ π¦ < (2nd β(πΉβ(πΊβπ‘))))) |
71 | 70 | simp3d 1145 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π¦ < (2nd β(πΉβ(πΊβπ‘)))) |
72 | 45, 47, 71 | ltled 11308 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π¦ β€ (2nd β(πΉβ(πΊβπ‘)))) |
73 | 38, 45, 47, 48, 72 | letrd 11317 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π‘ β π β§ π¦ β (π‘ β© (π΄[,]π΅)))) β π΄ β€ (2nd β(πΉβ(πΊβπ‘)))) |
74 | 73 | expr 458 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β π) β (π¦ β (π‘ β© (π΄[,]π΅)) β π΄ β€ (2nd β(πΉβ(πΊβπ‘))))) |
75 | 74 | exlimdv 1937 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β (βπ¦ π¦ β (π‘ β© (π΄[,]π΅)) β π΄ β€ (2nd β(πΉβ(πΊβπ‘))))) |
76 | 37, 75 | mpd 15 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β π΄ β€ (2nd β(πΉβ(πΊβπ‘)))) |
77 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β π΄ β€ π΅) |
78 | | breq2 5110 |
. . . . . . . . . . . 12
β’
((2nd β(πΉβ(πΊβπ‘))) = if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π΄ β€ (2nd β(πΉβ(πΊβπ‘))) β π΄ β€ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅))) |
79 | | breq2 5110 |
. . . . . . . . . . . 12
β’ (π΅ = if((2nd
β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π΄ β€ π΅ β π΄ β€ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅))) |
80 | 78, 79 | ifboth 4526 |
. . . . . . . . . . 11
β’ ((π΄ β€ (2nd
β(πΉβ(πΊβπ‘))) β§ π΄ β€ π΅) β π΄ β€ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅)) |
81 | 76, 77, 80 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β π΄ β€ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅)) |
82 | | min2 13115 |
. . . . . . . . . . 11
β’
(((2nd β(πΉβ(πΊβπ‘))) β β β§ π΅ β β) β if((2nd
β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β€ π΅) |
83 | 31, 32, 82 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β€ π΅) |
84 | | elicc2 13335 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΅ β β) β
(if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π΄[,]π΅) β (if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β β β§ π΄ β€ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β§ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β€ π΅))) |
85 | 2, 4, 84 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (if((2nd
β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π΄[,]π΅) β (if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β β β§ π΄ β€ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β§ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β€ π΅))) |
86 | 85 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β (if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π΄[,]π΅) β (if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β β β§ π΄ β€ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β§ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β€ π΅))) |
87 | 33, 81, 83, 86 | mpbir3and 1343 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π΄[,]π΅)) |
88 | 18, 87 | sseldd 3946 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β βͺ π) |
89 | | eluni2 4870 |
. . . . . . . 8
β’
(if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β βͺ π β βπ₯ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯) |
90 | 88, 89 | sylib 217 |
. . . . . . 7
β’ ((π β§ π‘ β π) β βπ₯ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯) |
91 | | simprl 770 |
. . . . . . . 8
β’ (((π β§ π‘ β π) β§ (π₯ β π β§ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯)) β π₯ β π) |
92 | | simprr 772 |
. . . . . . . . 9
β’ (((π β§ π‘ β π) β§ (π₯ β π β§ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯)) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯) |
93 | 87 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π‘ β π) β§ (π₯ β π β§ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯)) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π΄[,]π΅)) |
94 | | inelcm 4425 |
. . . . . . . . 9
β’
((if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯ β§ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π΄[,]π΅)) β (π₯ β© (π΄[,]π΅)) β β
) |
95 | 92, 93, 94 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π‘ β π) β§ (π₯ β π β§ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯)) β (π₯ β© (π΄[,]π΅)) β β
) |
96 | | ineq1 4166 |
. . . . . . . . . 10
β’ (π’ = π₯ β (π’ β© (π΄[,]π΅)) = (π₯ β© (π΄[,]π΅))) |
97 | 96 | neeq1d 3000 |
. . . . . . . . 9
β’ (π’ = π₯ β ((π’ β© (π΄[,]π΅)) β β
β (π₯ β© (π΄[,]π΅)) β β
)) |
98 | 97, 14 | elrab2 3649 |
. . . . . . . 8
β’ (π₯ β π β (π₯ β π β§ (π₯ β© (π΄[,]π΅)) β β
)) |
99 | 91, 95, 98 | sylanbrc 584 |
. . . . . . 7
β’ (((π β§ π‘ β π) β§ (π₯ β π β§ if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯)) β π₯ β π) |
100 | 90, 99, 92 | reximssdv 3166 |
. . . . . 6
β’ ((π β§ π‘ β π) β βπ₯ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯) |
101 | 100 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ‘ β π βπ₯ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯) |
102 | | eleq2 2823 |
. . . . . 6
β’ (π₯ = (ββπ‘) β (if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯ β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (ββπ‘))) |
103 | 102 | ac6sfi 9234 |
. . . . 5
β’ ((π β Fin β§ βπ‘ β π βπ₯ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β π₯) β ββ(β:πβΆπ β§ βπ‘ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (ββπ‘))) |
104 | 17, 101, 103 | syl2anc 585 |
. . . 4
β’ (π β ββ(β:πβΆπ β§ βπ‘ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (ββπ‘))) |
105 | 104 | adantr 482 |
. . 3
β’ ((π β§ (π§ β π β§ π΄ β π§)) β ββ(β:πβΆπ β§ βπ‘ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (ββπ‘))) |
106 | | 2fveq3 6848 |
. . . . . . . . . . 11
β’ (π₯ = π‘ β (πΉβ(πΊβπ₯)) = (πΉβ(πΊβπ‘))) |
107 | 106 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π₯ = π‘ β (2nd β(πΉβ(πΊβπ₯))) = (2nd β(πΉβ(πΊβπ‘)))) |
108 | 107 | breq1d 5116 |
. . . . . . . . 9
β’ (π₯ = π‘ β ((2nd β(πΉβ(πΊβπ₯))) β€ π΅ β (2nd β(πΉβ(πΊβπ‘))) β€ π΅)) |
109 | 108, 107 | ifbieq1d 4511 |
. . . . . . . 8
β’ (π₯ = π‘ β if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) = if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅)) |
110 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = π‘ β (ββπ₯) = (ββπ‘)) |
111 | 109, 110 | eleq12d 2828 |
. . . . . . 7
β’ (π₯ = π‘ β (if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (ββπ‘))) |
112 | 111 | cbvralvw 3224 |
. . . . . 6
β’
(βπ₯ β
π if((2nd
β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯) β βπ‘ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (ββπ‘)) |
113 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β π΄ β β) |
114 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β π΅ β β) |
115 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β π΄ β€ π΅) |
116 | | ovolicc2.4 |
. . . . . . . . 9
β’ π = seq1( + , ((abs β
β ) β πΉ)) |
117 | 26 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β πΉ:ββΆ( β€ β© (β
Γ β))) |
118 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β π β (π« ran ((,) β πΉ) β© Fin)) |
119 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β (π΄[,]π΅) β βͺ π) |
120 | 19 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β πΊ:πβΆβ) |
121 | 53 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) |
122 | | simprrl 780 |
. . . . . . . . 9
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β β:πβΆπ) |
123 | | simprrr 781 |
. . . . . . . . . 10
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)) |
124 | 111 | rspccva 3579 |
. . . . . . . . . 10
β’
((βπ₯ β
π if((2nd
β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯) β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (ββπ‘)) |
125 | 123, 124 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (ββπ‘)) |
126 | | simprlr 779 |
. . . . . . . . 9
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β π΄ β π§) |
127 | | simprll 778 |
. . . . . . . . . 10
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β π§ β π) |
128 | 8 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β π΄ β (π΄[,]π΅)) |
129 | | inelcm 4425 |
. . . . . . . . . . 11
β’ ((π΄ β π§ β§ π΄ β (π΄[,]π΅)) β (π§ β© (π΄[,]π΅)) β β
) |
130 | 126, 128,
129 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β (π§ β© (π΄[,]π΅)) β β
) |
131 | | ineq1 4166 |
. . . . . . . . . . . 12
β’ (π’ = π§ β (π’ β© (π΄[,]π΅)) = (π§ β© (π΄[,]π΅))) |
132 | 131 | neeq1d 3000 |
. . . . . . . . . . 11
β’ (π’ = π§ β ((π’ β© (π΄[,]π΅)) β β
β (π§ β© (π΄[,]π΅)) β β
)) |
133 | 132, 14 | elrab2 3649 |
. . . . . . . . . 10
β’ (π§ β π β (π§ β π β§ (π§ β© (π΄[,]π΅)) β β
)) |
134 | 127, 130,
133 | sylanbrc 584 |
. . . . . . . . 9
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β π§ β π) |
135 | | eqid 2733 |
. . . . . . . . 9
β’
seq1((β β
1st ), (β Γ {π§})) = seq1((β β 1st ), (β Γ
{π§})) |
136 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = π β (seq1((β β 1st ), (β Γ
{π§}))βπ) = (seq1((β β 1st ), (β Γ
{π§}))βπ)) |
137 | 136 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π = π β (π΅ β (seq1((β β 1st ), (β Γ
{π§}))βπ) β π΅ β (seq1((β β 1st ), (β Γ
{π§}))βπ))) |
138 | 137 | cbvrabv 3416 |
. . . . . . . . 9
β’ {π β β β£ π΅ β (seq1((β β 1st ),
(β Γ {π§}))βπ)} = {π β β β£ π΅ β (seq1((β β 1st ), (β Γ
{π§}))βπ)} |
139 | | eqid 2733 |
. . . . . . . . 9
β’
inf({π β
β β£ π΅ β
(seq1((β β
1st ), (β Γ {π§}))βπ)}, β, < ) = inf({π β β β£ π΅ β (seq1((β β 1st ), (β Γ
{π§}))βπ)}, β, <
) |
140 | 113, 114,
115, 116, 117, 118, 119, 120, 121, 14, 122, 125, 126, 134, 135, 138, 139 | ovolicc2lem4 24900 |
. . . . . . . 8
β’ ((π β§ ((π§ β π β§ π΄ β π§) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯)))) β (π΅ β π΄) β€ sup(ran π, β*, <
)) |
141 | 140 | anassrs 469 |
. . . . . . 7
β’ (((π β§ (π§ β π β§ π΄ β π§)) β§ (β:πβΆπ β§ βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯))) β (π΅ β π΄) β€ sup(ran π, β*, <
)) |
142 | 141 | expr 458 |
. . . . . 6
β’ (((π β§ (π§ β π β§ π΄ β π§)) β§ β:πβΆπ) β (βπ₯ β π if((2nd β(πΉβ(πΊβπ₯))) β€ π΅, (2nd β(πΉβ(πΊβπ₯))), π΅) β (ββπ₯) β (π΅ β π΄) β€ sup(ran π, β*, <
))) |
143 | 112, 142 | biimtrrid 242 |
. . . . 5
β’ (((π β§ (π§ β π β§ π΄ β π§)) β§ β:πβΆπ) β (βπ‘ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (ββπ‘) β (π΅ β π΄) β€ sup(ran π, β*, <
))) |
144 | 143 | expimpd 455 |
. . . 4
β’ ((π β§ (π§ β π β§ π΄ β π§)) β ((β:πβΆπ β§ βπ‘ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (ββπ‘)) β (π΅ β π΄) β€ sup(ran π, β*, <
))) |
145 | 144 | exlimdv 1937 |
. . 3
β’ ((π β§ (π§ β π β§ π΄ β π§)) β (ββ(β:πβΆπ β§ βπ‘ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (ββπ‘)) β (π΅ β π΄) β€ sup(ran π, β*, <
))) |
146 | 105, 145 | mpd 15 |
. 2
β’ ((π β§ (π§ β π β§ π΄ β π§)) β (π΅ β π΄) β€ sup(ran π, β*, <
)) |
147 | 11, 146 | rexlimddv 3155 |
1
β’ (π β (π΅ β π΄) β€ sup(ran π, β*, <
)) |