Step | Hyp | Ref
| Expression |
1 | | iccssxr 13407 |
. . 3
β’
(0[,]+β) β β* |
2 | | omeiunle.o |
. . . 4
β’ (π β π β OutMeas) |
3 | | omeiunle.x |
. . . 4
β’ π = βͺ
dom π |
4 | | omeiunle.nph |
. . . . . 6
β’
β²ππ |
5 | | omeiunle.e |
. . . . . . . . 9
β’ (π β πΈ:πβΆπ« π) |
6 | 5 | ffvelcdmda 7087 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΈβπ) β π« π) |
7 | | elpwi 4610 |
. . . . . . . 8
β’ ((πΈβπ) β π« π β (πΈβπ) β π) |
8 | 6, 7 | syl 17 |
. . . . . . 7
β’ ((π β§ π β π) β (πΈβπ) β π) |
9 | 8 | ex 414 |
. . . . . 6
β’ (π β (π β π β (πΈβπ) β π)) |
10 | 4, 9 | ralrimi 3255 |
. . . . 5
β’ (π β βπ β π (πΈβπ) β π) |
11 | | iunss 5049 |
. . . . 5
β’ (βͺ π β π (πΈβπ) β π β βπ β π (πΈβπ) β π) |
12 | 10, 11 | sylibr 233 |
. . . 4
β’ (π β βͺ π β π (πΈβπ) β π) |
13 | 2, 3, 12 | omecl 45219 |
. . 3
β’ (π β (πββͺ
π β π (πΈβπ)) β (0[,]+β)) |
14 | 1, 13 | sselid 3981 |
. 2
β’ (π β (πββͺ
π β π (πΈβπ)) β
β*) |
15 | 5 | ffnd 6719 |
. . . . 5
β’ (π β πΈ Fn π) |
16 | | omeiunle.z |
. . . . . . 7
β’ π =
(β€β₯βπ) |
17 | 16 | fvexi 6906 |
. . . . . 6
β’ π β V |
18 | 17 | a1i 11 |
. . . . 5
β’ (π β π β V) |
19 | | fnex 7219 |
. . . . 5
β’ ((πΈ Fn π β§ π β V) β πΈ β V) |
20 | 15, 18, 19 | syl2anc 585 |
. . . 4
β’ (π β πΈ β V) |
21 | | rnexg 7895 |
. . . 4
β’ (πΈ β V β ran πΈ β V) |
22 | 20, 21 | syl 17 |
. . 3
β’ (π β ran πΈ β V) |
23 | 2, 3 | omef 45212 |
. . . 4
β’ (π β π:π« πβΆ(0[,]+β)) |
24 | 5 | frnd 6726 |
. . . 4
β’ (π β ran πΈ β π« π) |
25 | 23, 24 | fssresd 6759 |
. . 3
β’ (π β (π βΎ ran πΈ):ran πΈβΆ(0[,]+β)) |
26 | 22, 25 | sge0xrcl 45101 |
. 2
β’ (π β
(Ξ£^β(π βΎ ran πΈ)) β
β*) |
27 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β π β OutMeas) |
28 | 27, 3, 8 | omecl 45219 |
. . . 4
β’ ((π β§ π β π) β (πβ(πΈβπ)) β (0[,]+β)) |
29 | | eqid 2733 |
. . . 4
β’ (π β π β¦ (πβ(πΈβπ))) = (π β π β¦ (πβ(πΈβπ))) |
30 | 4, 28, 29 | fmptdf 7117 |
. . 3
β’ (π β (π β π β¦ (πβ(πΈβπ))):πβΆ(0[,]+β)) |
31 | 18, 30 | sge0xrcl 45101 |
. 2
β’ (π β
(Ξ£^β(π β π β¦ (πβ(πΈβπ)))) β
β*) |
32 | | fvex 6905 |
. . . . . . . 8
β’ (πΈβπ) β V |
33 | 32 | rgenw 3066 |
. . . . . . 7
β’
βπ β
π (πΈβπ) β V |
34 | | dfiun3g 5964 |
. . . . . . 7
β’
(βπ β
π (πΈβπ) β V β βͺ π β π (πΈβπ) = βͺ ran (π β π β¦ (πΈβπ))) |
35 | 33, 34 | ax-mp 5 |
. . . . . 6
β’ βͺ π β π (πΈβπ) = βͺ ran (π β π β¦ (πΈβπ)) |
36 | 35 | a1i 11 |
. . . . 5
β’ (π β βͺ π β π (πΈβπ) = βͺ ran (π β π β¦ (πΈβπ))) |
37 | 5 | feqmptd 6961 |
. . . . . . . 8
β’ (π β πΈ = (π β π β¦ (πΈβπ))) |
38 | | omeiunle.ne |
. . . . . . . . . . 11
β’
β²ππΈ |
39 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²ππ |
40 | 38, 39 | nffv 6902 |
. . . . . . . . . 10
β’
β²π(πΈβπ) |
41 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π(πΈβπ) |
42 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π = π β (πΈβπ) = (πΈβπ)) |
43 | 40, 41, 42 | cbvmpt 5260 |
. . . . . . . . 9
β’ (π β π β¦ (πΈβπ)) = (π β π β¦ (πΈβπ)) |
44 | 43 | a1i 11 |
. . . . . . . 8
β’ (π β (π β π β¦ (πΈβπ)) = (π β π β¦ (πΈβπ))) |
45 | 37, 44 | eqtrd 2773 |
. . . . . . 7
β’ (π β πΈ = (π β π β¦ (πΈβπ))) |
46 | 45 | rneqd 5938 |
. . . . . 6
β’ (π β ran πΈ = ran (π β π β¦ (πΈβπ))) |
47 | 46 | unieqd 4923 |
. . . . 5
β’ (π β βͺ ran πΈ = βͺ ran (π β π β¦ (πΈβπ))) |
48 | 36, 47 | eqtr4d 2776 |
. . . 4
β’ (π β βͺ π β π (πΈβπ) = βͺ ran πΈ) |
49 | 48 | fveq2d 6896 |
. . 3
β’ (π β (πββͺ
π β π (πΈβπ)) = (πββͺ ran
πΈ)) |
50 | | fnrndomg 10531 |
. . . . . 6
β’ (π β V β (πΈ Fn π β ran πΈ βΌ π)) |
51 | 18, 15, 50 | sylc 65 |
. . . . 5
β’ (π β ran πΈ βΌ π) |
52 | 16 | uzct 43750 |
. . . . . 6
β’ π βΌ
Ο |
53 | 52 | a1i 11 |
. . . . 5
β’ (π β π βΌ Ο) |
54 | | domtr 9003 |
. . . . 5
β’ ((ran
πΈ βΌ π β§ π βΌ Ο) β ran πΈ βΌ
Ο) |
55 | 51, 53, 54 | syl2anc 585 |
. . . 4
β’ (π β ran πΈ βΌ Ο) |
56 | 2, 3, 24, 55 | omeunile 45221 |
. . 3
β’ (π β (πββͺ ran
πΈ) β€
(Ξ£^β(π βΎ ran πΈ))) |
57 | 49, 56 | eqbrtrd 5171 |
. 2
β’ (π β (πββͺ
π β π (πΈβπ)) β€
(Ξ£^β(π βΎ ran πΈ))) |
58 | | ltweuz 13926 |
. . . . . 6
β’ < We
(β€β₯βπ) |
59 | | weeq2 5666 |
. . . . . . 7
β’ (π =
(β€β₯βπ) β ( < We π β < We
(β€β₯βπ))) |
60 | 16, 59 | ax-mp 5 |
. . . . . 6
β’ ( < We
π β < We
(β€β₯βπ)) |
61 | 58, 60 | mpbir 230 |
. . . . 5
β’ < We
π |
62 | 61 | a1i 11 |
. . . 4
β’ (π β < We π) |
63 | 18, 23, 5, 62 | sge0resrn 45120 |
. . 3
β’ (π β
(Ξ£^β(π βΎ ran πΈ)) β€
(Ξ£^β(π β πΈ))) |
64 | | fcompt 7131 |
. . . . . 6
β’ ((π:π« πβΆ(0[,]+β) β§ πΈ:πβΆπ« π) β (π β πΈ) = (π β π β¦ (πβ(πΈβπ)))) |
65 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ |
66 | 65, 40 | nffv 6902 |
. . . . . . . 8
β’
β²π(πβ(πΈβπ)) |
67 | | nfcv 2904 |
. . . . . . . 8
β’
β²π(πβ(πΈβπ)) |
68 | | 2fveq3 6897 |
. . . . . . . 8
β’ (π = π β (πβ(πΈβπ)) = (πβ(πΈβπ))) |
69 | 66, 67, 68 | cbvmpt 5260 |
. . . . . . 7
β’ (π β π β¦ (πβ(πΈβπ))) = (π β π β¦ (πβ(πΈβπ))) |
70 | 69 | a1i 11 |
. . . . . 6
β’ ((π:π« πβΆ(0[,]+β) β§ πΈ:πβΆπ« π) β (π β π β¦ (πβ(πΈβπ))) = (π β π β¦ (πβ(πΈβπ)))) |
71 | 64, 70 | eqtrd 2773 |
. . . . 5
β’ ((π:π« πβΆ(0[,]+β) β§ πΈ:πβΆπ« π) β (π β πΈ) = (π β π β¦ (πβ(πΈβπ)))) |
72 | 23, 5, 71 | syl2anc 585 |
. . . 4
β’ (π β (π β πΈ) = (π β π β¦ (πβ(πΈβπ)))) |
73 | 72 | fveq2d 6896 |
. . 3
β’ (π β
(Ξ£^β(π β πΈ)) =
(Ξ£^β(π β π β¦ (πβ(πΈβπ))))) |
74 | 63, 73 | breqtrd 5175 |
. 2
β’ (π β
(Ξ£^β(π βΎ ran πΈ)) β€
(Ξ£^β(π β π β¦ (πβ(πΈβπ))))) |
75 | 14, 26, 31, 57, 74 | xrletrd 13141 |
1
β’ (π β (πββͺ
π β π (πΈβπ)) β€
(Ξ£^β(π β π β¦ (πβ(πΈβπ))))) |