Step | Hyp | Ref
| Expression |
1 | | mbfsup.5 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β β) |
2 | 1 | anassrs 469 |
. . . . . . 7
β’ (((π β§ π β π) β§ π₯ β π΄) β π΅ β β) |
3 | 2 | an32s 651 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ π β π) β π΅ β β) |
4 | 3 | fmpttd 7068 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅):πβΆβ) |
5 | 4 | frnd 6681 |
. . . 4
β’ ((π β§ π₯ β π΄) β ran (π β π β¦ π΅) β β) |
6 | | mbfsup.3 |
. . . . . . . . . 10
β’ (π β π β β€) |
7 | | uzid 12785 |
. . . . . . . . . 10
β’ (π β β€ β π β
(β€β₯βπ)) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
β’ (π β π β (β€β₯βπ)) |
9 | | mbfsup.1 |
. . . . . . . . 9
β’ π =
(β€β₯βπ) |
10 | 8, 9 | eleqtrrdi 2849 |
. . . . . . . 8
β’ (π β π β π) |
11 | 10 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β π β π) |
12 | | eqid 2737 |
. . . . . . . 8
β’ (π β π β¦ π΅) = (π β π β¦ π΅) |
13 | 12, 3 | dmmptd 6651 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β dom (π β π β¦ π΅) = π) |
14 | 11, 13 | eleqtrrd 2841 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β π β dom (π β π β¦ π΅)) |
15 | 14 | ne0d 4300 |
. . . . 5
β’ ((π β§ π₯ β π΄) β dom (π β π β¦ π΅) β β
) |
16 | | dm0rn0 5885 |
. . . . . 6
β’ (dom
(π β π β¦ π΅) = β
β ran (π β π β¦ π΅) = β
) |
17 | 16 | necon3bii 2997 |
. . . . 5
β’ (dom
(π β π β¦ π΅) β β
β ran (π β π β¦ π΅) β β
) |
18 | 15, 17 | sylib 217 |
. . . 4
β’ ((π β§ π₯ β π΄) β ran (π β π β¦ π΅) β β
) |
19 | | mbfsup.6 |
. . . . 5
β’ ((π β§ π₯ β π΄) β βπ¦ β β βπ β π π΅ β€ π¦) |
20 | 4 | ffnd 6674 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅) Fn π) |
21 | | breq1 5113 |
. . . . . . . . 9
β’ (π§ = ((π β π β¦ π΅)βπ) β (π§ β€ π¦ β ((π β π β¦ π΅)βπ) β€ π¦)) |
22 | 21 | ralrn 7043 |
. . . . . . . 8
β’ ((π β π β¦ π΅) Fn π β (βπ§ β ran (π β π β¦ π΅)π§ β€ π¦ β βπ β π ((π β π β¦ π΅)βπ) β€ π¦)) |
23 | 20, 22 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (βπ§ β ran (π β π β¦ π΅)π§ β€ π¦ β βπ β π ((π β π β¦ π΅)βπ) β€ π¦)) |
24 | | nffvmpt1 6858 |
. . . . . . . . . 10
β’
β²π((π β π β¦ π΅)βπ) |
25 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π
β€ |
26 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²ππ¦ |
27 | 24, 25, 26 | nfbr 5157 |
. . . . . . . . 9
β’
β²π((π β π β¦ π΅)βπ) β€ π¦ |
28 | | nfv 1918 |
. . . . . . . . 9
β’
β²π((π β π β¦ π΅)βπ) β€ π¦ |
29 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΅)βπ)) |
30 | 29 | breq1d 5120 |
. . . . . . . . 9
β’ (π = π β (((π β π β¦ π΅)βπ) β€ π¦ β ((π β π β¦ π΅)βπ) β€ π¦)) |
31 | 27, 28, 30 | cbvralw 3292 |
. . . . . . . 8
β’
(βπ β
π ((π β π β¦ π΅)βπ) β€ π¦ β βπ β π ((π β π β¦ π΅)βπ) β€ π¦) |
32 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π΄) β§ π β π) β π β π) |
33 | 12 | fvmpt2 6964 |
. . . . . . . . . . 11
β’ ((π β π β§ π΅ β β) β ((π β π β¦ π΅)βπ) = π΅) |
34 | 32, 3, 33 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π΄) β§ π β π) β ((π β π β¦ π΅)βπ) = π΅) |
35 | 34 | breq1d 5120 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΄) β§ π β π) β (((π β π β¦ π΅)βπ) β€ π¦ β π΅ β€ π¦)) |
36 | 35 | ralbidva 3173 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (βπ β π ((π β π β¦ π΅)βπ) β€ π¦ β βπ β π π΅ β€ π¦)) |
37 | 31, 36 | bitrid 283 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (βπ β π ((π β π β¦ π΅)βπ) β€ π¦ β βπ β π π΅ β€ π¦)) |
38 | 23, 37 | bitrd 279 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (βπ§ β ran (π β π β¦ π΅)π§ β€ π¦ β βπ β π π΅ β€ π¦)) |
39 | 38 | rexbidv 3176 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (βπ¦ β β βπ§ β ran (π β π β¦ π΅)π§ β€ π¦ β βπ¦ β β βπ β π π΅ β€ π¦)) |
40 | 19, 39 | mpbird 257 |
. . . 4
β’ ((π β§ π₯ β π΄) β βπ¦ β β βπ§ β ran (π β π β¦ π΅)π§ β€ π¦) |
41 | 5, 18, 40 | suprcld 12125 |
. . 3
β’ ((π β§ π₯ β π΄) β sup(ran (π β π β¦ π΅), β, < ) β
β) |
42 | | mbfsup.2 |
. . 3
β’ πΊ = (π₯ β π΄ β¦ sup(ran (π β π β¦ π΅), β, < )) |
43 | 41, 42 | fmptd 7067 |
. 2
β’ (π β πΊ:π΄βΆβ) |
44 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β π₯ β π΄) |
45 | | ltso 11242 |
. . . . . . . . . . . . . 14
β’ < Or
β |
46 | 45 | supex 9406 |
. . . . . . . . . . . . 13
β’ sup(ran
(π β π β¦ π΅), β, < ) β V |
47 | 42 | fvmpt2 6964 |
. . . . . . . . . . . . 13
β’ ((π₯ β π΄ β§ sup(ran (π β π β¦ π΅), β, < ) β V) β (πΊβπ₯) = sup(ran (π β π β¦ π΅), β, < )) |
48 | 44, 46, 47 | sylancl 587 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β (πΊβπ₯) = sup(ran (π β π β¦ π΅), β, < )) |
49 | 48 | breq2d 5122 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β (π‘ < (πΊβπ₯) β π‘ < sup(ran (π β π β¦ π΅), β, < ))) |
50 | 5, 18, 40 | 3jca 1129 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β (ran (π β π β¦ π΅) β β β§ ran (π β π β¦ π΅) β β
β§ βπ¦ β β βπ§ β ran (π β π β¦ π΅)π§ β€ π¦)) |
51 | 50 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β (ran (π β π β¦ π΅) β β β§ ran (π β π β¦ π΅) β β
β§ βπ¦ β β βπ§ β ran (π β π β¦ π΅)π§ β€ π¦)) |
52 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β π‘ β β) |
53 | | suprlub 12126 |
. . . . . . . . . . . 12
β’ (((ran
(π β π β¦ π΅) β β β§ ran (π β π β¦ π΅) β β
β§ βπ¦ β β βπ§ β ran (π β π β¦ π΅)π§ β€ π¦) β§ π‘ β β) β (π‘ < sup(ran (π β π β¦ π΅), β, < ) β βπ§ β ran (π β π β¦ π΅)π‘ < π§)) |
54 | 51, 52, 53 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β (π‘ < sup(ran (π β π β¦ π΅), β, < ) β βπ§ β ran (π β π β¦ π΅)π‘ < π§)) |
55 | 20 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β (π β π β¦ π΅) Fn π) |
56 | | breq2 5114 |
. . . . . . . . . . . . . 14
β’ (π§ = ((π β π β¦ π΅)βπ) β (π‘ < π§ β π‘ < ((π β π β¦ π΅)βπ))) |
57 | 56 | rexrn 7042 |
. . . . . . . . . . . . 13
β’ ((π β π β¦ π΅) Fn π β (βπ§ β ran (π β π β¦ π΅)π‘ < π§ β βπ β π π‘ < ((π β π β¦ π΅)βπ))) |
58 | 55, 57 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β (βπ§ β ran (π β π β¦ π΅)π‘ < π§ β βπ β π π‘ < ((π β π β¦ π΅)βπ))) |
59 | | nfcv 2908 |
. . . . . . . . . . . . . . 15
β’
β²ππ‘ |
60 | | nfcv 2908 |
. . . . . . . . . . . . . . 15
β’
β²π
< |
61 | 59, 60, 24 | nfbr 5157 |
. . . . . . . . . . . . . 14
β’
β²π π‘ < ((π β π β¦ π΅)βπ) |
62 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π π‘ < ((π β π β¦ π΅)βπ) |
63 | 29 | breq2d 5122 |
. . . . . . . . . . . . . 14
β’ (π = π β (π‘ < ((π β π β¦ π΅)βπ) β π‘ < ((π β π β¦ π΅)βπ))) |
64 | 61, 62, 63 | cbvrexw 3293 |
. . . . . . . . . . . . 13
β’
(βπ β
π π‘ < ((π β π β¦ π΅)βπ) β βπ β π π‘ < ((π β π β¦ π΅)βπ)) |
65 | 12 | fvmpt2i 6963 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β ((π β π β¦ π΅)βπ) = ( I βπ΅)) |
66 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β π΄ β¦ π΅) = (π₯ β π΄ β¦ π΅) |
67 | 66 | fvmpt2i 6963 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π΄ β ((π₯ β π΄ β¦ π΅)βπ₯) = ( I βπ΅)) |
68 | 67 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β π΄) β ((π₯ β π΄ β¦ π΅)βπ₯) = ( I βπ΅)) |
69 | 68 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β π΄) β ( I βπ΅) = ((π₯ β π΄ β¦ π΅)βπ₯)) |
70 | 65, 69 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π΄) β§ π β π) β ((π β π β¦ π΅)βπ) = ((π₯ β π΄ β¦ π΅)βπ₯)) |
71 | 70 | breq2d 5122 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΄) β§ π β π) β (π‘ < ((π β π β¦ π΅)βπ) β π‘ < ((π₯ β π΄ β¦ π΅)βπ₯))) |
72 | 71 | rexbidva 3174 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΄) β (βπ β π π‘ < ((π β π β¦ π΅)βπ) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ₯))) |
73 | 72 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β (βπ β π π‘ < ((π β π β¦ π΅)βπ) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ₯))) |
74 | 64, 73 | bitrid 283 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β (βπ β π π‘ < ((π β π β¦ π΅)βπ) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ₯))) |
75 | 58, 74 | bitrd 279 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β (βπ§ β ran (π β π β¦ π΅)π‘ < π§ β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ₯))) |
76 | 49, 54, 75 | 3bitrd 305 |
. . . . . . . . . 10
β’ (((π β§ π‘ β β) β§ π₯ β π΄) β (π‘ < (πΊβπ₯) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ₯))) |
77 | 76 | ralrimiva 3144 |
. . . . . . . . 9
β’ ((π β§ π‘ β β) β βπ₯ β π΄ (π‘ < (πΊβπ₯) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ₯))) |
78 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π§(π‘ < (πΊβπ₯) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ₯)) |
79 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π₯π‘ |
80 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π₯
< |
81 | | nfmpt1 5218 |
. . . . . . . . . . . . . 14
β’
β²π₯(π₯ β π΄ β¦ sup(ran (π β π β¦ π΅), β, < )) |
82 | 42, 81 | nfcxfr 2906 |
. . . . . . . . . . . . 13
β’
β²π₯πΊ |
83 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²π₯π§ |
84 | 82, 83 | nffv 6857 |
. . . . . . . . . . . 12
β’
β²π₯(πΊβπ§) |
85 | 79, 80, 84 | nfbr 5157 |
. . . . . . . . . . 11
β’
β²π₯ π‘ < (πΊβπ§) |
86 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π₯π |
87 | | nffvmpt1 6858 |
. . . . . . . . . . . . 13
β’
β²π₯((π₯ β π΄ β¦ π΅)βπ§) |
88 | 79, 80, 87 | nfbr 5157 |
. . . . . . . . . . . 12
β’
β²π₯ π‘ < ((π₯ β π΄ β¦ π΅)βπ§) |
89 | 86, 88 | nfrexw 3299 |
. . . . . . . . . . 11
β’
β²π₯βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ§) |
90 | 85, 89 | nfbi 1907 |
. . . . . . . . . 10
β’
β²π₯(π‘ < (πΊβπ§) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ§)) |
91 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β (πΊβπ₯) = (πΊβπ§)) |
92 | 91 | breq2d 5122 |
. . . . . . . . . . 11
β’ (π₯ = π§ β (π‘ < (πΊβπ₯) β π‘ < (πΊβπ§))) |
93 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π₯ = π§ β ((π₯ β π΄ β¦ π΅)βπ₯) = ((π₯ β π΄ β¦ π΅)βπ§)) |
94 | 93 | breq2d 5122 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β (π‘ < ((π₯ β π΄ β¦ π΅)βπ₯) β π‘ < ((π₯ β π΄ β¦ π΅)βπ§))) |
95 | 94 | rexbidv 3176 |
. . . . . . . . . . 11
β’ (π₯ = π§ β (βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ₯) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ§))) |
96 | 92, 95 | bibi12d 346 |
. . . . . . . . . 10
β’ (π₯ = π§ β ((π‘ < (πΊβπ₯) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ₯)) β (π‘ < (πΊβπ§) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ§)))) |
97 | 78, 90, 96 | cbvralw 3292 |
. . . . . . . . 9
β’
(βπ₯ β
π΄ (π‘ < (πΊβπ₯) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ₯)) β βπ§ β π΄ (π‘ < (πΊβπ§) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ§))) |
98 | 77, 97 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π‘ β β) β βπ§ β π΄ (π‘ < (πΊβπ§) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ§))) |
99 | 98 | r19.21bi 3237 |
. . . . . . 7
β’ (((π β§ π‘ β β) β§ π§ β π΄) β (π‘ < (πΊβπ§) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ§))) |
100 | 43 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β β) β πΊ:π΄βΆβ) |
101 | 100 | ffvelcdmda 7040 |
. . . . . . . 8
β’ (((π β§ π‘ β β) β§ π§ β π΄) β (πΊβπ§) β β) |
102 | | rexr 11208 |
. . . . . . . . . 10
β’ (π‘ β β β π‘ β
β*) |
103 | 102 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π‘ β β) β§ π§ β π΄) β π‘ β β*) |
104 | | elioopnf 13367 |
. . . . . . . . 9
β’ (π‘ β β*
β ((πΊβπ§) β (π‘(,)+β) β ((πΊβπ§) β β β§ π‘ < (πΊβπ§)))) |
105 | 103, 104 | syl 17 |
. . . . . . . 8
β’ (((π β§ π‘ β β) β§ π§ β π΄) β ((πΊβπ§) β (π‘(,)+β) β ((πΊβπ§) β β β§ π‘ < (πΊβπ§)))) |
106 | 101, 105 | mpbirand 706 |
. . . . . . 7
β’ (((π β§ π‘ β β) β§ π§ β π΄) β ((πΊβπ§) β (π‘(,)+β) β π‘ < (πΊβπ§))) |
107 | 103 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π‘ β β) β§ π§ β π΄) β§ π β π) β π‘ β β*) |
108 | | elioopnf 13367 |
. . . . . . . . . 10
β’ (π‘ β β*
β (((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β) β (((π₯ β π΄ β¦ π΅)βπ§) β β β§ π‘ < ((π₯ β π΄ β¦ π΅)βπ§)))) |
109 | 107, 108 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π‘ β β) β§ π§ β π΄) β§ π β π) β (((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β) β (((π₯ β π΄ β¦ π΅)βπ§) β β β§ π‘ < ((π₯ β π΄ β¦ π΅)βπ§)))) |
110 | 2 | fmpttd 7068 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
111 | 110 | ffvelcdmda 7040 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π§ β π΄) β ((π₯ β π΄ β¦ π΅)βπ§) β β) |
112 | 111 | biantrurd 534 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π§ β π΄) β (π‘ < ((π₯ β π΄ β¦ π΅)βπ§) β (((π₯ β π΄ β¦ π΅)βπ§) β β β§ π‘ < ((π₯ β π΄ β¦ π΅)βπ§)))) |
113 | 112 | an32s 651 |
. . . . . . . . . 10
β’ (((π β§ π§ β π΄) β§ π β π) β (π‘ < ((π₯ β π΄ β¦ π΅)βπ§) β (((π₯ β π΄ β¦ π΅)βπ§) β β β§ π‘ < ((π₯ β π΄ β¦ π΅)βπ§)))) |
114 | 113 | adantllr 718 |
. . . . . . . . 9
β’ ((((π β§ π‘ β β) β§ π§ β π΄) β§ π β π) β (π‘ < ((π₯ β π΄ β¦ π΅)βπ§) β (((π₯ β π΄ β¦ π΅)βπ§) β β β§ π‘ < ((π₯ β π΄ β¦ π΅)βπ§)))) |
115 | 109, 114 | bitr4d 282 |
. . . . . . . 8
β’ ((((π β§ π‘ β β) β§ π§ β π΄) β§ π β π) β (((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β) β π‘ < ((π₯ β π΄ β¦ π΅)βπ§))) |
116 | 115 | rexbidva 3174 |
. . . . . . 7
β’ (((π β§ π‘ β β) β§ π§ β π΄) β (βπ β π ((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β) β βπ β π π‘ < ((π₯ β π΄ β¦ π΅)βπ§))) |
117 | 99, 106, 116 | 3bitr4d 311 |
. . . . . 6
β’ (((π β§ π‘ β β) β§ π§ β π΄) β ((πΊβπ§) β (π‘(,)+β) β βπ β π ((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β))) |
118 | 117 | pm5.32da 580 |
. . . . 5
β’ ((π β§ π‘ β β) β ((π§ β π΄ β§ (πΊβπ§) β (π‘(,)+β)) β (π§ β π΄ β§ βπ β π ((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β)))) |
119 | 43 | ffnd 6674 |
. . . . . . 7
β’ (π β πΊ Fn π΄) |
120 | 119 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β β) β πΊ Fn π΄) |
121 | | elpreima 7013 |
. . . . . 6
β’ (πΊ Fn π΄ β (π§ β (β‘πΊ β (π‘(,)+β)) β (π§ β π΄ β§ (πΊβπ§) β (π‘(,)+β)))) |
122 | 120, 121 | syl 17 |
. . . . 5
β’ ((π β§ π‘ β β) β (π§ β (β‘πΊ β (π‘(,)+β)) β (π§ β π΄ β§ (πΊβπ§) β (π‘(,)+β)))) |
123 | | eliun 4963 |
. . . . . 6
β’ (π§ β βͺ π β π (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β βπ β π π§ β (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β))) |
124 | 110 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) Fn π΄) |
125 | | elpreima 7013 |
. . . . . . . . . 10
β’ ((π₯ β π΄ β¦ π΅) Fn π΄ β (π§ β (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β (π§ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β)))) |
126 | 124, 125 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π§ β (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β (π§ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β)))) |
127 | 126 | rexbidva 3174 |
. . . . . . . 8
β’ (π β (βπ β π π§ β (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β βπ β π (π§ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β)))) |
128 | 127 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β β) β (βπ β π π§ β (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β βπ β π (π§ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β)))) |
129 | | r19.42v 3188 |
. . . . . . 7
β’
(βπ β
π (π§ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β)) β (π§ β π΄ β§ βπ β π ((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β))) |
130 | 128, 129 | bitrdi 287 |
. . . . . 6
β’ ((π β§ π‘ β β) β (βπ β π π§ β (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β (π§ β π΄ β§ βπ β π ((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β)))) |
131 | 123, 130 | bitrid 283 |
. . . . 5
β’ ((π β§ π‘ β β) β (π§ β βͺ
π β π (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β (π§ β π΄ β§ βπ β π ((π₯ β π΄ β¦ π΅)βπ§) β (π‘(,)+β)))) |
132 | 118, 122,
131 | 3bitr4d 311 |
. . . 4
β’ ((π β§ π‘ β β) β (π§ β (β‘πΊ β (π‘(,)+β)) β π§ β βͺ
π β π (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)))) |
133 | 132 | eqrdv 2735 |
. . 3
β’ ((π β§ π‘ β β) β (β‘πΊ β (π‘(,)+β)) = βͺ π β π (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β))) |
134 | | zex 12515 |
. . . . . . 7
β’ β€
β V |
135 | | uzssz 12791 |
. . . . . . 7
β’
(β€β₯βπ) β β€ |
136 | | ssdomg 8947 |
. . . . . . 7
β’ (β€
β V β ((β€β₯βπ) β β€ β
(β€β₯βπ) βΌ β€)) |
137 | 134, 135,
136 | mp2 9 |
. . . . . 6
β’
(β€β₯βπ) βΌ β€ |
138 | 9, 137 | eqbrtri 5131 |
. . . . 5
β’ π βΌ
β€ |
139 | | znnen 16101 |
. . . . 5
β’ β€
β β |
140 | | domentr 8960 |
. . . . 5
β’ ((π βΌ β€ β§ β€
β β) β π
βΌ β) |
141 | 138, 139,
140 | mp2an 691 |
. . . 4
β’ π βΌ
β |
142 | | mbfsup.4 |
. . . . . . 7
β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) |
143 | | mbfima 25010 |
. . . . . . 7
β’ (((π₯ β π΄ β¦ π΅) β MblFn β§ (π₯ β π΄ β¦ π΅):π΄βΆβ) β (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β dom
vol) |
144 | 142, 110,
143 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β π) β (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β dom
vol) |
145 | 144 | ralrimiva 3144 |
. . . . 5
β’ (π β βπ β π (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β dom
vol) |
146 | 145 | adantr 482 |
. . . 4
β’ ((π β§ π‘ β β) β βπ β π (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β dom
vol) |
147 | | iunmbl2 24937 |
. . . 4
β’ ((π βΌ β β§
βπ β π (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β dom vol) β βͺ π β π (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β dom
vol) |
148 | 141, 146,
147 | sylancr 588 |
. . 3
β’ ((π β§ π‘ β β) β βͺ π β π (β‘(π₯ β π΄ β¦ π΅) β (π‘(,)+β)) β dom
vol) |
149 | 133, 148 | eqeltrd 2838 |
. 2
β’ ((π β§ π‘ β β) β (β‘πΊ β (π‘(,)+β)) β dom
vol) |
150 | 43, 149 | ismbf3d 25034 |
1
β’ (π β πΊ β MblFn) |