Step | Hyp | Ref
| Expression |
1 | | ovolicc2.5 |
. . . . . 6
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
2 | | inss2 4193 |
. . . . . 6
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
3 | | fss 6689 |
. . . . . 6
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β Γ β)) β πΉ:ββΆ(β Γ
β)) |
4 | 1, 2, 3 | sylancl 587 |
. . . . 5
β’ (π β πΉ:ββΆ(β Γ
β)) |
5 | | ovolicc2.8 |
. . . . . 6
β’ (π β πΊ:πβΆβ) |
6 | 5 | ffvelcdmda 7039 |
. . . . 5
β’ ((π β§ π β π) β (πΊβπ) β β) |
7 | | fvco3 6944 |
. . . . 5
β’ ((πΉ:ββΆ(β Γ
β) β§ (πΊβπ) β β) β (((,) β πΉ)β(πΊβπ)) = ((,)β(πΉβ(πΊβπ)))) |
8 | 4, 6, 7 | syl2an2r 684 |
. . . 4
β’ ((π β§ π β π) β (((,) β πΉ)β(πΊβπ)) = ((,)β(πΉβ(πΊβπ)))) |
9 | | ovolicc2.9 |
. . . . . 6
β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) |
10 | 9 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ‘ β π (((,) β πΉ)β(πΊβπ‘)) = π‘) |
11 | | 2fveq3 6851 |
. . . . . . 7
β’ (π‘ = π β (((,) β πΉ)β(πΊβπ‘)) = (((,) β πΉ)β(πΊβπ))) |
12 | | id 22 |
. . . . . . 7
β’ (π‘ = π β π‘ = π) |
13 | 11, 12 | eqeq12d 2749 |
. . . . . 6
β’ (π‘ = π β ((((,) β πΉ)β(πΊβπ‘)) = π‘ β (((,) β πΉ)β(πΊβπ)) = π)) |
14 | 13 | rspccva 3582 |
. . . . 5
β’
((βπ‘ β
π (((,) β πΉ)β(πΊβπ‘)) = π‘ β§ π β π) β (((,) β πΉ)β(πΊβπ)) = π) |
15 | 10, 14 | sylan 581 |
. . . 4
β’ ((π β§ π β π) β (((,) β πΉ)β(πΊβπ)) = π) |
16 | 4 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β πΉ:ββΆ(β Γ
β)) |
17 | 16, 6 | ffvelcdmd 7040 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβ(πΊβπ)) β (β Γ
β)) |
18 | | 1st2nd2 7964 |
. . . . . . 7
β’ ((πΉβ(πΊβπ)) β (β Γ β) β
(πΉβ(πΊβπ)) = β¨(1st β(πΉβ(πΊβπ))), (2nd β(πΉβ(πΊβπ)))β©) |
19 | 17, 18 | syl 17 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβ(πΊβπ)) = β¨(1st β(πΉβ(πΊβπ))), (2nd β(πΉβ(πΊβπ)))β©) |
20 | 19 | fveq2d 6850 |
. . . . 5
β’ ((π β§ π β π) β ((,)β(πΉβ(πΊβπ))) = ((,)ββ¨(1st
β(πΉβ(πΊβπ))), (2nd β(πΉβ(πΊβπ)))β©)) |
21 | | df-ov 7364 |
. . . . 5
β’
((1st β(πΉβ(πΊβπ)))(,)(2nd β(πΉβ(πΊβπ)))) = ((,)ββ¨(1st
β(πΉβ(πΊβπ))), (2nd β(πΉβ(πΊβπ)))β©) |
22 | 20, 21 | eqtr4di 2791 |
. . . 4
β’ ((π β§ π β π) β ((,)β(πΉβ(πΊβπ))) = ((1st β(πΉβ(πΊβπ)))(,)(2nd β(πΉβ(πΊβπ))))) |
23 | 8, 15, 22 | 3eqtr3d 2781 |
. . 3
β’ ((π β§ π β π) β π = ((1st β(πΉβ(πΊβπ)))(,)(2nd β(πΉβ(πΊβπ))))) |
24 | 23 | eleq2d 2820 |
. 2
β’ ((π β§ π β π) β (π β π β π β ((1st β(πΉβ(πΊβπ)))(,)(2nd β(πΉβ(πΊβπ)))))) |
25 | | xp1st 7957 |
. . . 4
β’ ((πΉβ(πΊβπ)) β (β Γ β) β
(1st β(πΉβ(πΊβπ))) β β) |
26 | 17, 25 | syl 17 |
. . 3
β’ ((π β§ π β π) β (1st β(πΉβ(πΊβπ))) β β) |
27 | | xp2nd 7958 |
. . . 4
β’ ((πΉβ(πΊβπ)) β (β Γ β) β
(2nd β(πΉβ(πΊβπ))) β β) |
28 | 17, 27 | syl 17 |
. . 3
β’ ((π β§ π β π) β (2nd β(πΉβ(πΊβπ))) β β) |
29 | | rexr 11209 |
. . . 4
β’
((1st β(πΉβ(πΊβπ))) β β β (1st
β(πΉβ(πΊβπ))) β
β*) |
30 | | rexr 11209 |
. . . 4
β’
((2nd β(πΉβ(πΊβπ))) β β β (2nd
β(πΉβ(πΊβπ))) β
β*) |
31 | | elioo2 13314 |
. . . 4
β’
(((1st β(πΉβ(πΊβπ))) β β* β§
(2nd β(πΉβ(πΊβπ))) β β*) β
(π β ((1st
β(πΉβ(πΊβπ)))(,)(2nd β(πΉβ(πΊβπ)))) β (π β β β§ (1st
β(πΉβ(πΊβπ))) < π β§ π < (2nd β(πΉβ(πΊβπ)))))) |
32 | 29, 30, 31 | syl2an 597 |
. . 3
β’
(((1st β(πΉβ(πΊβπ))) β β β§ (2nd
β(πΉβ(πΊβπ))) β β) β (π β ((1st
β(πΉβ(πΊβπ)))(,)(2nd β(πΉβ(πΊβπ)))) β (π β β β§ (1st
β(πΉβ(πΊβπ))) < π β§ π < (2nd β(πΉβ(πΊβπ)))))) |
33 | 26, 28, 32 | syl2anc 585 |
. 2
β’ ((π β§ π β π) β (π β ((1st β(πΉβ(πΊβπ)))(,)(2nd β(πΉβ(πΊβπ)))) β (π β β β§ (1st
β(πΉβ(πΊβπ))) < π β§ π < (2nd β(πΉβ(πΊβπ)))))) |
34 | 24, 33 | bitrd 279 |
1
β’ ((π β§ π β π) β (π β π β (π β β β§ (1st
β(πΉβ(πΊβπ))) < π β§ π < (2nd β(πΉβ(πΊβπ)))))) |