Step | Hyp | Ref
| Expression |
1 | | ulmrel 25753 |
. . . 4
β’ Rel
(βπ’βπ) |
2 | 1 | brrelex12i 5692 |
. . 3
β’ (πΉ(βπ’βπ)πΊ β (πΉ β V β§ πΊ β V)) |
3 | 2 | a1i 11 |
. 2
β’ (π β π β (πΉ(βπ’βπ)πΊ β (πΉ β V β§ πΊ β V))) |
4 | | 3simpa 1149 |
. . . 4
β’ ((πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) β (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ)) |
5 | | fvex 6860 |
. . . . . . 7
β’
(β€β₯βπ) β V |
6 | | fex 7181 |
. . . . . . 7
β’ ((πΉ:(β€β₯βπ)βΆ(β
βm π) β§
(β€β₯βπ) β V) β πΉ β V) |
7 | 5, 6 | mpan2 690 |
. . . . . 6
β’ (πΉ:(β€β₯βπ)βΆ(β
βm π)
β πΉ β
V) |
8 | 7 | a1i 11 |
. . . . 5
β’ (π β π β (πΉ:(β€β₯βπ)βΆ(β
βm π)
β πΉ β
V)) |
9 | | fex 7181 |
. . . . . 6
β’ ((πΊ:πβΆβ β§ π β π) β πΊ β V) |
10 | 9 | expcom 415 |
. . . . 5
β’ (π β π β (πΊ:πβΆβ β πΊ β V)) |
11 | 8, 10 | anim12d 610 |
. . . 4
β’ (π β π β ((πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ) β (πΉ β V β§ πΊ β V))) |
12 | 4, 11 | syl5 34 |
. . 3
β’ (π β π β ((πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) β (πΉ β V β§ πΊ β V))) |
13 | 12 | rexlimdvw 3158 |
. 2
β’ (π β π β (βπ β β€ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) β (πΉ β V β§ πΊ β V))) |
14 | | df-ulm 25752 |
. . . . . 6
β’
βπ’ = (π β V β¦ {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π ) β§
π¦:π βΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)}) |
15 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π β (β βm π ) = (β βm
π)) |
16 | 15 | feq3d 6660 |
. . . . . . . . 9
β’ (π = π β (π:(β€β₯βπ)βΆ(β
βm π )
β π:(β€β₯βπ)βΆ(β
βm π))) |
17 | | feq2 6655 |
. . . . . . . . 9
β’ (π = π β (π¦:π βΆβ β π¦:πβΆβ)) |
18 | | raleq 3312 |
. . . . . . . . . . 11
β’ (π = π β (βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ β βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)) |
19 | 18 | rexralbidv 3215 |
. . . . . . . . . 10
β’ (π = π β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)) |
20 | 19 | ralbidv 3175 |
. . . . . . . . 9
β’ (π = π β (βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ β βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)) |
21 | 16, 17, 20 | 3anbi123d 1437 |
. . . . . . . 8
β’ (π = π β ((π:(β€β₯βπ)βΆ(β
βm π ) β§
π¦:π βΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯) β (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯))) |
22 | 21 | rexbidv 3176 |
. . . . . . 7
β’ (π = π β (βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π ) β§
π¦:π βΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯) β βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯))) |
23 | 22 | opabbidv 5176 |
. . . . . 6
β’ (π = π β {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π ) β§
π¦:π βΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)} = {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)}) |
24 | | elex 3466 |
. . . . . 6
β’ (π β π β π β V) |
25 | | simpr1 1195 |
. . . . . . . . . . . . 13
β’ ((π β π β§ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)) β π:(β€β₯βπ)βΆ(β
βm π)) |
26 | | uzssz 12791 |
. . . . . . . . . . . . 13
β’
(β€β₯βπ) β β€ |
27 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’ (β
βm π)
β V |
28 | | zex 12515 |
. . . . . . . . . . . . . 14
β’ β€
β V |
29 | | elpm2r 8790 |
. . . . . . . . . . . . . 14
β’
((((β βm π) β V β§ β€ β V) β§
(π:(β€β₯βπ)βΆ(β
βm π) β§
(β€β₯βπ) β β€)) β π β ((β βm π) βpm
β€)) |
30 | 27, 28, 29 | mpanl12 701 |
. . . . . . . . . . . . 13
β’ ((π:(β€β₯βπ)βΆ(β
βm π) β§
(β€β₯βπ) β β€) β π β ((β βm π) βpm
β€)) |
31 | 25, 26, 30 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β π β§ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)) β π β ((β βm π) βpm
β€)) |
32 | | simpr2 1196 |
. . . . . . . . . . . . 13
β’ ((π β π β§ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)) β π¦:πβΆβ) |
33 | | cnex 11139 |
. . . . . . . . . . . . . 14
β’ β
β V |
34 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)) β π β π) |
35 | | elmapg 8785 |
. . . . . . . . . . . . . 14
β’ ((β
β V β§ π β
π) β (π¦ β (β
βm π)
β π¦:πβΆβ)) |
36 | 33, 34, 35 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π β π β§ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)) β (π¦ β (β βm π) β π¦:πβΆβ)) |
37 | 32, 36 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π β π β§ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)) β π¦ β (β βm π)) |
38 | 31, 37 | jca 513 |
. . . . . . . . . . 11
β’ ((π β π β§ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)) β (π β ((β βm π) βpm β€)
β§ π¦ β (β
βm π))) |
39 | 38 | ex 414 |
. . . . . . . . . 10
β’ (π β π β ((π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯) β (π β ((β βm π) βpm β€)
β§ π¦ β (β
βm π)))) |
40 | 39 | rexlimdvw 3158 |
. . . . . . . . 9
β’ (π β π β (βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯) β (π β ((β βm π) βpm β€)
β§ π¦ β (β
βm π)))) |
41 | 40 | ssopab2dv 5513 |
. . . . . . . 8
β’ (π β π β {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)} β {β¨π, π¦β© β£ (π β ((β βm π) βpm β€)
β§ π¦ β (β
βm π))}) |
42 | | df-xp 5644 |
. . . . . . . 8
β’
(((β βm π) βpm β€) Γ
(β βm π)) = {β¨π, π¦β© β£ (π β ((β βm π) βpm β€)
β§ π¦ β (β
βm π))} |
43 | 41, 42 | sseqtrrdi 4000 |
. . . . . . 7
β’ (π β π β {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)} β (((β βm
π) βpm
β€) Γ (β βm π))) |
44 | | ovex 7395 |
. . . . . . . . 9
β’ ((β
βm π)
βpm β€) β V |
45 | 44, 27 | xpex 7692 |
. . . . . . . 8
β’
(((β βm π) βpm β€) Γ
(β βm π)) β V |
46 | 45 | ssex 5283 |
. . . . . . 7
β’
({β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)} β (((β βm
π) βpm
β€) Γ (β βm π)) β {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)} β V) |
47 | 43, 46 | syl 17 |
. . . . . 6
β’ (π β π β {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)} β V) |
48 | 14, 23, 24, 47 | fvmptd3 6976 |
. . . . 5
β’ (π β π β
(βπ’βπ) = {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)}) |
49 | 48 | breqd 5121 |
. . . 4
β’ (π β π β (πΉ(βπ’βπ)πΊ β πΉ{β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)}πΊ)) |
50 | | simpl 484 |
. . . . . . . 8
β’ ((π = πΉ β§ π¦ = πΊ) β π = πΉ) |
51 | 50 | feq1d 6658 |
. . . . . . 7
β’ ((π = πΉ β§ π¦ = πΊ) β (π:(β€β₯βπ)βΆ(β
βm π)
β πΉ:(β€β₯βπ)βΆ(β
βm π))) |
52 | | simpr 486 |
. . . . . . . 8
β’ ((π = πΉ β§ π¦ = πΊ) β π¦ = πΊ) |
53 | 52 | feq1d 6658 |
. . . . . . 7
β’ ((π = πΉ β§ π¦ = πΊ) β (π¦:πβΆβ β πΊ:πβΆβ)) |
54 | 50 | fveq1d 6849 |
. . . . . . . . . . . . . 14
β’ ((π = πΉ β§ π¦ = πΊ) β (πβπ) = (πΉβπ)) |
55 | 54 | fveq1d 6849 |
. . . . . . . . . . . . 13
β’ ((π = πΉ β§ π¦ = πΊ) β ((πβπ)βπ§) = ((πΉβπ)βπ§)) |
56 | 52 | fveq1d 6849 |
. . . . . . . . . . . . 13
β’ ((π = πΉ β§ π¦ = πΊ) β (π¦βπ§) = (πΊβπ§)) |
57 | 55, 56 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ ((π = πΉ β§ π¦ = πΊ) β (((πβπ)βπ§) β (π¦βπ§)) = (((πΉβπ)βπ§) β (πΊβπ§))) |
58 | 57 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π = πΉ β§ π¦ = πΊ) β (absβ(((πβπ)βπ§) β (π¦βπ§))) = (absβ(((πΉβπ)βπ§) β (πΊβπ§)))) |
59 | 58 | breq1d 5120 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π¦ = πΊ) β ((absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ β (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯)) |
60 | 59 | ralbidv 3175 |
. . . . . . . . 9
β’ ((π = πΉ β§ π¦ = πΊ) β (βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ β βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯)) |
61 | 60 | rexralbidv 3215 |
. . . . . . . 8
β’ ((π = πΉ β§ π¦ = πΊ) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯)) |
62 | 61 | ralbidv 3175 |
. . . . . . 7
β’ ((π = πΉ β§ π¦ = πΊ) β (βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ β βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯)) |
63 | 51, 53, 62 | 3anbi123d 1437 |
. . . . . 6
β’ ((π = πΉ β§ π¦ = πΊ) β ((π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯) β (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) |
64 | 63 | rexbidv 3176 |
. . . . 5
β’ ((π = πΉ β§ π¦ = πΊ) β (βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯) β βπ β β€ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) |
65 | | eqid 2737 |
. . . . 5
β’
{β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)} = {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)} |
66 | 64, 65 | brabga 5496 |
. . . 4
β’ ((πΉ β V β§ πΊ β V) β (πΉ{β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π) β§
π¦:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)}πΊ β βπ β β€ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) |
67 | 49, 66 | sylan9bb 511 |
. . 3
β’ ((π β π β§ (πΉ β V β§ πΊ β V)) β (πΉ(βπ’βπ)πΊ β βπ β β€ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) |
68 | 67 | ex 414 |
. 2
β’ (π β π β ((πΉ β V β§ πΊ β V) β (πΉ(βπ’βπ)πΊ β βπ β β€ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯)))) |
69 | 3, 13, 68 | pm5.21ndd 381 |
1
β’ (π β π β (πΉ(βπ’βπ)πΊ β βπ β β€ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) |