Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’ ran
(π¦ β
β* β¦ (π¦(,]+β)) = ran (π¦ β β* β¦ (π¦(,]+β)) |
2 | | eqid 2733 |
. . . 4
β’ ran
(π¦ β
β* β¦ (-β[,)π¦)) = ran (π¦ β β* β¦
(-β[,)π¦)) |
3 | 1, 2 | leordtval2 22716 |
. . 3
β’
(ordTopβ β€ ) = (topGenβ(fiβ(ran (π¦ β β* β¦ (π¦(,]+β)) βͺ ran (π¦ β β*
β¦ (-β[,)π¦))))) |
4 | | fvex 6905 |
. . . 4
β’
(fiβran πΉ)
β V |
5 | | fvex 6905 |
. . . . . 6
β’
(ordTopβ β€ ) β V |
6 | | lecldbas.1 |
. . . . . . . 8
β’ πΉ = (π₯ β ran [,] β¦ (β*
β π₯)) |
7 | | iccf 13425 |
. . . . . . . . . . 11
β’
[,]:(β* Γ β*)βΆπ«
β* |
8 | | ffn 6718 |
. . . . . . . . . . 11
β’
([,]:(β* Γ β*)βΆπ«
β* β [,] Fn (β* Γ
β*)) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
β’ [,] Fn
(β* Γ β*) |
10 | | ovelrn 7583 |
. . . . . . . . . 10
β’ ([,] Fn
(β* Γ β*) β (π₯ β ran [,] β βπ β β*
βπ β
β* π₯ =
(π[,]π))) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . 9
β’ (π₯ β ran [,] β
βπ β
β* βπ β β* π₯ = (π[,]π)) |
12 | | difeq2 4117 |
. . . . . . . . . . . 12
β’ (π₯ = (π[,]π) β (β* β π₯) = (β* β
(π[,]π))) |
13 | | iccordt 22718 |
. . . . . . . . . . . . 13
β’ (π[,]π) β (Clsdβ(ordTopβ β€
)) |
14 | | letopuni 22711 |
. . . . . . . . . . . . . 14
β’
β* = βͺ (ordTopβ β€
) |
15 | 14 | cldopn 22535 |
. . . . . . . . . . . . 13
β’ ((π[,]π) β (Clsdβ(ordTopβ β€ ))
β (β* β (π[,]π)) β (ordTopβ β€
)) |
16 | 13, 15 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(β* β (π[,]π)) β (ordTopβ β€
) |
17 | 12, 16 | eqeltrdi 2842 |
. . . . . . . . . . 11
β’ (π₯ = (π[,]π) β (β* β π₯) β (ordTopβ β€
)) |
18 | 17 | rexlimivw 3152 |
. . . . . . . . . 10
β’
(βπ β
β* π₯ =
(π[,]π) β (β* β π₯) β (ordTopβ β€
)) |
19 | 18 | rexlimivw 3152 |
. . . . . . . . 9
β’
(βπ β
β* βπ β β* π₯ = (π[,]π) β (β* β π₯) β (ordTopβ β€
)) |
20 | 11, 19 | sylbi 216 |
. . . . . . . 8
β’ (π₯ β ran [,] β
(β* β π₯) β (ordTopβ β€
)) |
21 | 6, 20 | fmpti 7112 |
. . . . . . 7
β’ πΉ:ran [,]βΆ(ordTopβ
β€ ) |
22 | | frn 6725 |
. . . . . . 7
β’ (πΉ:ran [,]βΆ(ordTopβ
β€ ) β ran πΉ β
(ordTopβ β€ )) |
23 | 21, 22 | ax-mp 5 |
. . . . . 6
β’ ran πΉ β (ordTopβ β€
) |
24 | 5, 23 | ssexi 5323 |
. . . . 5
β’ ran πΉ β V |
25 | | eqid 2733 |
. . . . . . . 8
β’ (π¦ β β*
β¦ (π¦(,]+β)) =
(π¦ β
β* β¦ (π¦(,]+β)) |
26 | | mnfxr 11271 |
. . . . . . . . . . 11
β’ -β
β β* |
27 | | fnovrn 7582 |
. . . . . . . . . . 11
β’ (([,] Fn
(β* Γ β*) β§ -β β
β* β§ π¦
β β*) β (-β[,]π¦) β ran [,]) |
28 | 9, 26, 27 | mp3an12 1452 |
. . . . . . . . . 10
β’ (π¦ β β*
β (-β[,]π¦)
β ran [,]) |
29 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π¦ β β*
β -β β β*) |
30 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π¦ β β*
β π¦ β
β*) |
31 | | pnfxr 11268 |
. . . . . . . . . . . . . . 15
β’ +β
β β* |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π¦ β β*
β +β β β*) |
33 | | mnfle 13114 |
. . . . . . . . . . . . . 14
β’ (π¦ β β*
β -β β€ π¦) |
34 | | pnfge 13110 |
. . . . . . . . . . . . . 14
β’ (π¦ β β*
β π¦ β€
+β) |
35 | | df-icc 13331 |
. . . . . . . . . . . . . . 15
β’ [,] =
(π β
β*, π
β β* β¦ {π β β* β£ (π β€ π β§ π β€ π)}) |
36 | | df-ioc 13329 |
. . . . . . . . . . . . . . 15
β’ (,] =
(π β
β*, π
β β* β¦ {π β β* β£ (π < π β§ π β€ π)}) |
37 | | xrltnle 11281 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β*
β§ π§ β
β*) β (π¦ < π§ β Β¬ π§ β€ π¦)) |
38 | | xrletr 13137 |
. . . . . . . . . . . . . . 15
β’ ((π§ β β*
β§ π¦ β
β* β§ +β β β*) β ((π§ β€ π¦ β§ π¦ β€ +β) β π§ β€ +β)) |
39 | | xrlelttr 13135 |
. . . . . . . . . . . . . . . 16
β’
((-β β β* β§ π¦ β β* β§ π§ β β*)
β ((-β β€ π¦
β§ π¦ < π§) β -β < π§)) |
40 | | xrltle 13128 |
. . . . . . . . . . . . . . . . 17
β’
((-β β β* β§ π§ β β*) β (-β
< π§ β -β β€
π§)) |
41 | 40 | 3adant2 1132 |
. . . . . . . . . . . . . . . 16
β’
((-β β β* β§ π¦ β β* β§ π§ β β*)
β (-β < π§
β -β β€ π§)) |
42 | 39, 41 | syld 47 |
. . . . . . . . . . . . . . 15
β’
((-β β β* β§ π¦ β β* β§ π§ β β*)
β ((-β β€ π¦
β§ π¦ < π§) β -β β€ π§)) |
43 | 35, 36, 37, 35, 38, 42 | ixxun 13340 |
. . . . . . . . . . . . . 14
β’
(((-β β β* β§ π¦ β β* β§ +β
β β*) β§ (-β β€ π¦ β§ π¦ β€ +β)) β ((-β[,]π¦) βͺ (π¦(,]+β)) =
(-β[,]+β)) |
44 | 29, 30, 32, 33, 34, 43 | syl32anc 1379 |
. . . . . . . . . . . . 13
β’ (π¦ β β*
β ((-β[,]π¦)
βͺ (π¦(,]+β)) =
(-β[,]+β)) |
45 | | iccmax 13400 |
. . . . . . . . . . . . 13
β’
(-β[,]+β) = β* |
46 | 44, 45 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (π¦ β β*
β ((-β[,]π¦)
βͺ (π¦(,]+β)) =
β*) |
47 | | iccssxr 13407 |
. . . . . . . . . . . . 13
β’
(-β[,]π¦)
β β* |
48 | 35, 36, 37 | ixxdisj 13339 |
. . . . . . . . . . . . . 14
β’
((-β β β* β§ π¦ β β* β§ +β
β β*) β ((-β[,]π¦) β© (π¦(,]+β)) = β
) |
49 | 26, 31, 48 | mp3an13 1453 |
. . . . . . . . . . . . 13
β’ (π¦ β β*
β ((-β[,]π¦)
β© (π¦(,]+β)) =
β
) |
50 | | uneqdifeq 4493 |
. . . . . . . . . . . . 13
β’
(((-β[,]π¦)
β β* β§ ((-β[,]π¦) β© (π¦(,]+β)) = β
) β
(((-β[,]π¦) βͺ
(π¦(,]+β)) =
β* β (β* β (-β[,]π¦)) = (π¦(,]+β))) |
51 | 47, 49, 50 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π¦ β β*
β (((-β[,]π¦)
βͺ (π¦(,]+β)) =
β* β (β* β (-β[,]π¦)) = (π¦(,]+β))) |
52 | 46, 51 | mpbid 231 |
. . . . . . . . . . 11
β’ (π¦ β β*
β (β* β (-β[,]π¦)) = (π¦(,]+β)) |
53 | 52 | eqcomd 2739 |
. . . . . . . . . 10
β’ (π¦ β β*
β (π¦(,]+β) =
(β* β (-β[,]π¦))) |
54 | | difeq2 4117 |
. . . . . . . . . . 11
β’ (π₯ = (-β[,]π¦) β (β*
β π₯) =
(β* β (-β[,]π¦))) |
55 | 54 | rspceeqv 3634 |
. . . . . . . . . 10
β’
(((-β[,]π¦)
β ran [,] β§ (π¦(,]+β) = (β* β
(-β[,]π¦))) β
βπ₯ β ran
[,](π¦(,]+β) =
(β* β π₯)) |
56 | 28, 53, 55 | syl2anc 585 |
. . . . . . . . 9
β’ (π¦ β β*
β βπ₯ β ran
[,](π¦(,]+β) =
(β* β π₯)) |
57 | | xrex 12971 |
. . . . . . . . . . 11
β’
β* β V |
58 | 57 | difexi 5329 |
. . . . . . . . . 10
β’
(β* β π₯) β V |
59 | 6, 58 | elrnmpti 5960 |
. . . . . . . . 9
β’ ((π¦(,]+β) β ran πΉ β βπ₯ β ran [,](π¦(,]+β) =
(β* β π₯)) |
60 | 56, 59 | sylibr 233 |
. . . . . . . 8
β’ (π¦ β β*
β (π¦(,]+β)
β ran πΉ) |
61 | 25, 60 | fmpti 7112 |
. . . . . . 7
β’ (π¦ β β*
β¦ (π¦(,]+β)):β*βΆran
πΉ |
62 | | frn 6725 |
. . . . . . 7
β’ ((π¦ β β*
β¦ (π¦(,]+β)):β*βΆran
πΉ β ran (π¦ β β*
β¦ (π¦(,]+β))
β ran πΉ) |
63 | 61, 62 | ax-mp 5 |
. . . . . 6
β’ ran
(π¦ β
β* β¦ (π¦(,]+β)) β ran πΉ |
64 | | eqid 2733 |
. . . . . . . 8
β’ (π¦ β β*
β¦ (-β[,)π¦)) =
(π¦ β
β* β¦ (-β[,)π¦)) |
65 | | fnovrn 7582 |
. . . . . . . . . . 11
β’ (([,] Fn
(β* Γ β*) β§ π¦ β β* β§ +β
β β*) β (π¦[,]+β) β ran [,]) |
66 | 9, 31, 65 | mp3an13 1453 |
. . . . . . . . . 10
β’ (π¦ β β*
β (π¦[,]+β)
β ran [,]) |
67 | | df-ico 13330 |
. . . . . . . . . . . . . . 15
β’ [,) =
(π β
β*, π
β β* β¦ {π β β* β£ (π β€ π β§ π < π)}) |
68 | | xrlenlt 11279 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β*
β§ π§ β
β*) β (π¦ β€ π§ β Β¬ π§ < π¦)) |
69 | | xrltletr 13136 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β β*
β§ π¦ β
β* β§ +β β β*) β ((π§ < π¦ β§ π¦ β€ +β) β π§ < +β)) |
70 | | xrltle 13128 |
. . . . . . . . . . . . . . . . 17
β’ ((π§ β β*
β§ +β β β*) β (π§ < +β β π§ β€ +β)) |
71 | 70 | 3adant2 1132 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β β*
β§ π¦ β
β* β§ +β β β*) β (π§ < +β β π§ β€
+β)) |
72 | 69, 71 | syld 47 |
. . . . . . . . . . . . . . 15
β’ ((π§ β β*
β§ π¦ β
β* β§ +β β β*) β ((π§ < π¦ β§ π¦ β€ +β) β π§ β€ +β)) |
73 | | xrletr 13137 |
. . . . . . . . . . . . . . 15
β’
((-β β β* β§ π¦ β β* β§ π§ β β*)
β ((-β β€ π¦
β§ π¦ β€ π§) β -β β€ π§)) |
74 | 67, 35, 68, 35, 72, 73 | ixxun 13340 |
. . . . . . . . . . . . . 14
β’
(((-β β β* β§ π¦ β β* β§ +β
β β*) β§ (-β β€ π¦ β§ π¦ β€ +β)) β ((-β[,)π¦) βͺ (π¦[,]+β)) =
(-β[,]+β)) |
75 | 29, 30, 32, 33, 34, 74 | syl32anc 1379 |
. . . . . . . . . . . . 13
β’ (π¦ β β*
β ((-β[,)π¦)
βͺ (π¦[,]+β)) =
(-β[,]+β)) |
76 | | uncom 4154 |
. . . . . . . . . . . . 13
β’
((-β[,)π¦)
βͺ (π¦[,]+β)) =
((π¦[,]+β) βͺ
(-β[,)π¦)) |
77 | 75, 76, 45 | 3eqtr3g 2796 |
. . . . . . . . . . . 12
β’ (π¦ β β*
β ((π¦[,]+β)
βͺ (-β[,)π¦)) =
β*) |
78 | | iccssxr 13407 |
. . . . . . . . . . . . 13
β’ (π¦[,]+β) β
β* |
79 | | incom 4202 |
. . . . . . . . . . . . . 14
β’ ((π¦[,]+β) β©
(-β[,)π¦)) =
((-β[,)π¦) β©
(π¦[,]+β)) |
80 | 67, 35, 68 | ixxdisj 13339 |
. . . . . . . . . . . . . . 15
β’
((-β β β* β§ π¦ β β* β§ +β
β β*) β ((-β[,)π¦) β© (π¦[,]+β)) = β
) |
81 | 26, 31, 80 | mp3an13 1453 |
. . . . . . . . . . . . . 14
β’ (π¦ β β*
β ((-β[,)π¦)
β© (π¦[,]+β)) =
β
) |
82 | 79, 81 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ (π¦ β β*
β ((π¦[,]+β)
β© (-β[,)π¦)) =
β
) |
83 | | uneqdifeq 4493 |
. . . . . . . . . . . . 13
β’ (((π¦[,]+β) β
β* β§ ((π¦[,]+β) β© (-β[,)π¦)) = β
) β (((π¦[,]+β) βͺ
(-β[,)π¦)) =
β* β (β* β (π¦[,]+β)) = (-β[,)π¦))) |
84 | 78, 82, 83 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π¦ β β*
β (((π¦[,]+β)
βͺ (-β[,)π¦)) =
β* β (β* β (π¦[,]+β)) = (-β[,)π¦))) |
85 | 77, 84 | mpbid 231 |
. . . . . . . . . . 11
β’ (π¦ β β*
β (β* β (π¦[,]+β)) = (-β[,)π¦)) |
86 | 85 | eqcomd 2739 |
. . . . . . . . . 10
β’ (π¦ β β*
β (-β[,)π¦) =
(β* β (π¦[,]+β))) |
87 | | difeq2 4117 |
. . . . . . . . . . 11
β’ (π₯ = (π¦[,]+β) β (β*
β π₯) =
(β* β (π¦[,]+β))) |
88 | 87 | rspceeqv 3634 |
. . . . . . . . . 10
β’ (((π¦[,]+β) β ran [,]
β§ (-β[,)π¦) =
(β* β (π¦[,]+β))) β βπ₯ β ran [,](-β[,)π¦) = (β* β
π₯)) |
89 | 66, 86, 88 | syl2anc 585 |
. . . . . . . . 9
β’ (π¦ β β*
β βπ₯ β ran
[,](-β[,)π¦) =
(β* β π₯)) |
90 | 6, 58 | elrnmpti 5960 |
. . . . . . . . 9
β’
((-β[,)π¦)
β ran πΉ β
βπ₯ β ran
[,](-β[,)π¦) =
(β* β π₯)) |
91 | 89, 90 | sylibr 233 |
. . . . . . . 8
β’ (π¦ β β*
β (-β[,)π¦)
β ran πΉ) |
92 | 64, 91 | fmpti 7112 |
. . . . . . 7
β’ (π¦ β β*
β¦ (-β[,)π¦)):β*βΆran πΉ |
93 | | frn 6725 |
. . . . . . 7
β’ ((π¦ β β*
β¦ (-β[,)π¦)):β*βΆran πΉ β ran (π¦ β β* β¦
(-β[,)π¦)) β ran
πΉ) |
94 | 92, 93 | ax-mp 5 |
. . . . . 6
β’ ran
(π¦ β
β* β¦ (-β[,)π¦)) β ran πΉ |
95 | 63, 94 | unssi 4186 |
. . . . 5
β’ (ran
(π¦ β
β* β¦ (π¦(,]+β)) βͺ ran (π¦ β β* β¦
(-β[,)π¦))) β
ran πΉ |
96 | | fiss 9419 |
. . . . 5
β’ ((ran
πΉ β V β§ (ran
(π¦ β
β* β¦ (π¦(,]+β)) βͺ ran (π¦ β β* β¦
(-β[,)π¦))) β
ran πΉ) β
(fiβ(ran (π¦ β
β* β¦ (π¦(,]+β)) βͺ ran (π¦ β β* β¦
(-β[,)π¦)))) β
(fiβran πΉ)) |
97 | 24, 95, 96 | mp2an 691 |
. . . 4
β’
(fiβ(ran (π¦
β β* β¦ (π¦(,]+β)) βͺ ran (π¦ β β* β¦
(-β[,)π¦)))) β
(fiβran πΉ) |
98 | | tgss 22471 |
. . . 4
β’
(((fiβran πΉ)
β V β§ (fiβ(ran (π¦ β β* β¦ (π¦(,]+β)) βͺ ran (π¦ β β*
β¦ (-β[,)π¦))))
β (fiβran πΉ))
β (topGenβ(fiβ(ran (π¦ β β* β¦ (π¦(,]+β)) βͺ ran (π¦ β β*
β¦ (-β[,)π¦)))))
β (topGenβ(fiβran πΉ))) |
99 | 4, 97, 98 | mp2an 691 |
. . 3
β’
(topGenβ(fiβ(ran (π¦ β β* β¦ (π¦(,]+β)) βͺ ran (π¦ β β*
β¦ (-β[,)π¦)))))
β (topGenβ(fiβran πΉ)) |
100 | 3, 99 | eqsstri 4017 |
. 2
β’
(ordTopβ β€ ) β (topGenβ(fiβran πΉ)) |
101 | | letop 22710 |
. . 3
β’
(ordTopβ β€ ) β Top |
102 | | tgfiss 22494 |
. . 3
β’
(((ordTopβ β€ ) β Top β§ ran πΉ β (ordTopβ β€ )) β
(topGenβ(fiβran πΉ)) β (ordTopβ β€
)) |
103 | 101, 23, 102 | mp2an 691 |
. 2
β’
(topGenβ(fiβran πΉ)) β (ordTopβ β€
) |
104 | 100, 103 | eqssi 3999 |
1
β’
(ordTopβ β€ ) = (topGenβ(fiβran πΉ)) |