Step | Hyp | Ref
| Expression |
1 | | eleq1 2822 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ฅ โ ๐ต โ ๐ โ ๐ต)) |
2 | | eleq1 2822 |
. . . . . 6
โข (๐ฆ = ๐ โ (๐ฆ โ ๐ต โ ๐ โ ๐ต)) |
3 | 1, 2 | bi2anan9 638 |
. . . . 5
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ โ ๐ต โง ๐ โ ๐ต))) |
4 | | simpl 484 |
. . . . . . 7
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ๐ฅ = ๐) |
5 | 4 | breq2d 5118 |
. . . . . 6
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ( 0 < ๐ฅ โ 0 < ๐)) |
6 | 4 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (๐ ยท ๐ฅ) = (๐ ยท ๐)) |
7 | | simpr 486 |
. . . . . . . 8
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ๐ฆ = ๐) |
8 | 6, 7 | breq12d 5119 |
. . . . . . 7
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ((๐ ยท ๐ฅ) < ๐ฆ โ (๐ ยท ๐) < ๐)) |
9 | 8 | ralbidv 3171 |
. . . . . 6
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ โ โ๐ โ โ (๐ ยท ๐) < ๐)) |
10 | 5, 9 | anbi12d 632 |
. . . . 5
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ) โ ( 0 < ๐ โง โ๐ โ โ (๐ ยท ๐) < ๐))) |
11 | 3, 10 | anbi12d 632 |
. . . 4
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ)) โ ((๐ โ ๐ต โง ๐ โ ๐ต) โง ( 0 < ๐ โง โ๐ โ โ (๐ ยท ๐) < ๐)))) |
12 | | eqid 2733 |
. . . 4
โข
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ))} = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ))} |
13 | 11, 12 | brabga 5492 |
. . 3
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ))}๐ โ ((๐ โ ๐ต โง ๐ โ ๐ต) โง ( 0 < ๐ โง โ๐ โ โ (๐ ยท ๐) < ๐)))) |
14 | 13 | 3adant1 1131 |
. 2
โข ((๐ โ ๐ โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ))}๐ โ ((๐ โ ๐ต โง ๐ โ ๐ต) โง ( 0 < ๐ โง โ๐ โ โ (๐ ยท ๐) < ๐)))) |
15 | | elex 3462 |
. . . . 5
โข (๐ โ ๐ โ ๐ โ V) |
16 | 15 | 3ad2ant1 1134 |
. . . 4
โข ((๐ โ ๐ โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ๐ โ V) |
17 | | fveq2 6843 |
. . . . . . . . . 10
โข (๐ค = ๐ โ (Baseโ๐ค) = (Baseโ๐)) |
18 | | inftm.b |
. . . . . . . . . 10
โข ๐ต = (Baseโ๐) |
19 | 17, 18 | eqtr4di 2791 |
. . . . . . . . 9
โข (๐ค = ๐ โ (Baseโ๐ค) = ๐ต) |
20 | 19 | eleq2d 2820 |
. . . . . . . 8
โข (๐ค = ๐ โ (๐ฅ โ (Baseโ๐ค) โ ๐ฅ โ ๐ต)) |
21 | 19 | eleq2d 2820 |
. . . . . . . 8
โข (๐ค = ๐ โ (๐ฆ โ (Baseโ๐ค) โ ๐ฆ โ ๐ต)) |
22 | 20, 21 | anbi12d 632 |
. . . . . . 7
โข (๐ค = ๐ โ ((๐ฅ โ (Baseโ๐ค) โง ๐ฆ โ (Baseโ๐ค)) โ (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต))) |
23 | | fveq2 6843 |
. . . . . . . . . 10
โข (๐ค = ๐ โ (0gโ๐ค) = (0gโ๐)) |
24 | | inftm.0 |
. . . . . . . . . 10
โข 0 =
(0gโ๐) |
25 | 23, 24 | eqtr4di 2791 |
. . . . . . . . 9
โข (๐ค = ๐ โ (0gโ๐ค) = 0 ) |
26 | | fveq2 6843 |
. . . . . . . . . 10
โข (๐ค = ๐ โ (ltโ๐ค) = (ltโ๐)) |
27 | | inftm.l |
. . . . . . . . . 10
โข < =
(ltโ๐) |
28 | 26, 27 | eqtr4di 2791 |
. . . . . . . . 9
โข (๐ค = ๐ โ (ltโ๐ค) = < ) |
29 | | eqidd 2734 |
. . . . . . . . 9
โข (๐ค = ๐ โ ๐ฅ = ๐ฅ) |
30 | 25, 28, 29 | breq123d 5120 |
. . . . . . . 8
โข (๐ค = ๐ โ ((0gโ๐ค)(ltโ๐ค)๐ฅ โ 0 < ๐ฅ)) |
31 | | fveq2 6843 |
. . . . . . . . . . . 12
โข (๐ค = ๐ โ (.gโ๐ค) = (.gโ๐)) |
32 | | inftm.x |
. . . . . . . . . . . 12
โข ยท =
(.gโ๐) |
33 | 31, 32 | eqtr4di 2791 |
. . . . . . . . . . 11
โข (๐ค = ๐ โ (.gโ๐ค) = ยท ) |
34 | 33 | oveqd 7375 |
. . . . . . . . . 10
โข (๐ค = ๐ โ (๐(.gโ๐ค)๐ฅ) = (๐ ยท ๐ฅ)) |
35 | | eqidd 2734 |
. . . . . . . . . 10
โข (๐ค = ๐ โ ๐ฆ = ๐ฆ) |
36 | 34, 28, 35 | breq123d 5120 |
. . . . . . . . 9
โข (๐ค = ๐ โ ((๐(.gโ๐ค)๐ฅ)(ltโ๐ค)๐ฆ โ (๐ ยท ๐ฅ) < ๐ฆ)) |
37 | 36 | ralbidv 3171 |
. . . . . . . 8
โข (๐ค = ๐ โ (โ๐ โ โ (๐(.gโ๐ค)๐ฅ)(ltโ๐ค)๐ฆ โ โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ)) |
38 | 30, 37 | anbi12d 632 |
. . . . . . 7
โข (๐ค = ๐ โ (((0gโ๐ค)(ltโ๐ค)๐ฅ โง โ๐ โ โ (๐(.gโ๐ค)๐ฅ)(ltโ๐ค)๐ฆ) โ ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ))) |
39 | 22, 38 | anbi12d 632 |
. . . . . 6
โข (๐ค = ๐ โ (((๐ฅ โ (Baseโ๐ค) โง ๐ฆ โ (Baseโ๐ค)) โง ((0gโ๐ค)(ltโ๐ค)๐ฅ โง โ๐ โ โ (๐(.gโ๐ค)๐ฅ)(ltโ๐ค)๐ฆ)) โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ)))) |
40 | 39 | opabbidv 5172 |
. . . . 5
โข (๐ค = ๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (Baseโ๐ค) โง ๐ฆ โ (Baseโ๐ค)) โง ((0gโ๐ค)(ltโ๐ค)๐ฅ โง โ๐ โ โ (๐(.gโ๐ค)๐ฅ)(ltโ๐ค)๐ฆ))} = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ))}) |
41 | | df-inftm 32063 |
. . . . 5
โข โ
= (๐ค โ V โฆ
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (Baseโ๐ค) โง ๐ฆ โ (Baseโ๐ค)) โง ((0gโ๐ค)(ltโ๐ค)๐ฅ โง โ๐ โ โ (๐(.gโ๐ค)๐ฅ)(ltโ๐ค)๐ฆ))}) |
42 | 18 | fvexi 6857 |
. . . . . . 7
โข ๐ต โ V |
43 | 42, 42 | xpex 7688 |
. . . . . 6
โข (๐ต ร ๐ต) โ V |
44 | | opabssxp 5725 |
. . . . . 6
โข
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ))} โ (๐ต ร ๐ต) |
45 | 43, 44 | ssexi 5280 |
. . . . 5
โข
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ))} โ V |
46 | 40, 41, 45 | fvmpt 6949 |
. . . 4
โข (๐ โ V โ
(โโ๐) =
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ))}) |
47 | 16, 46 | syl 17 |
. . 3
โข ((๐ โ ๐ โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (โโ๐) = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ))}) |
48 | 47 | breqd 5117 |
. 2
โข ((๐ โ ๐ โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐(โโ๐)๐ โ ๐{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ( 0 < ๐ฅ โง โ๐ โ โ (๐ ยท ๐ฅ) < ๐ฆ))}๐)) |
49 | | 3simpc 1151 |
. . 3
โข ((๐ โ ๐ โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐ต โง ๐ โ ๐ต)) |
50 | 49 | biantrurd 534 |
. 2
โข ((๐ โ ๐ โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (( 0 < ๐ โง โ๐ โ โ (๐ ยท ๐) < ๐) โ ((๐ โ ๐ต โง ๐ โ ๐ต) โง ( 0 < ๐ โง โ๐ โ โ (๐ ยท ๐) < ๐)))) |
51 | 14, 48, 50 | 3bitr4d 311 |
1
โข ((๐ โ ๐ โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐(โโ๐)๐ โ ( 0 < ๐ โง โ๐ โ โ (๐ ยท ๐) < ๐))) |