Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
2 | 1 | breq1d 5116 |
. . . . . 6
β’ (π = π β ((πΉβπ) β€ (πΉβπ) β (πΉβπ) β€ (πΉβπ))) |
3 | | breq1 5109 |
. . . . . 6
β’ (π = π β (πππ β πππ)) |
4 | 2, 3 | bibi12d 346 |
. . . . 5
β’ (π = π β (((πΉβπ) β€ (πΉβπ) β πππ) β ((πΉβπ) β€ (πΉβπ) β πππ))) |
5 | 4 | imbi2d 341 |
. . . 4
β’ (π = π β ((π β ((πΉβπ) β€ (πΉβπ) β πππ)) β (π β ((πΉβπ) β€ (πΉβπ) β πππ)))) |
6 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
7 | 6 | breq2d 5118 |
. . . . . 6
β’ (π = π β ((πΉβπ) β€ (πΉβπ) β (πΉβπ) β€ (πΉβπ))) |
8 | | breq2 5110 |
. . . . . 6
β’ (π = π β (πππ β πππ)) |
9 | 7, 8 | bibi12d 346 |
. . . . 5
β’ (π = π β (((πΉβπ) β€ (πΉβπ) β πππ) β ((πΉβπ) β€ (πΉβπ) β πππ))) |
10 | 9 | imbi2d 341 |
. . . 4
β’ (π = π β ((π β ((πΉβπ) β€ (πΉβπ) β πππ)) β (π β ((πΉβπ) β€ (πΉβπ) β πππ)))) |
11 | | imasless.f |
. . . . . . . . . . . 12
β’ (π β πΉ:πβontoβπ΅) |
12 | | fofn 6759 |
. . . . . . . . . . . 12
β’ (πΉ:πβontoβπ΅ β πΉ Fn π) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΉ Fn π) |
14 | 13 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β πΉ Fn π) |
15 | 14 | fndmd 6608 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β dom πΉ = π) |
16 | 15 | rexeqdv 3315 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β (βπ β dom πΉ(ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)) β βπ β π (ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)))) |
17 | | fnbrfvb 6896 |
. . . . . . . . . . . 12
β’ ((πΉ Fn π β§ π β π) β ((πΉβπ) = (πΉβπ) β ππΉ(πΉβπ))) |
18 | 14, 17 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β ((πΉβπ) = (πΉβπ) β ππΉ(πΉβπ))) |
19 | 18 | anbi1d 631 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β (((πΉβπ) = (πΉβπ) β§ π(πΉ β π)(πΉβπ)) β (ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)))) |
20 | | ancom 462 |
. . . . . . . . . . . . . . 15
β’ ((πππ β§ ππΉ(πΉβπ)) β (ππΉ(πΉβπ) β§ πππ)) |
21 | | vex 3450 |
. . . . . . . . . . . . . . . . . 18
β’ π β V |
22 | | fvex 6856 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉβπ) β V |
23 | 21, 22 | breldm 5865 |
. . . . . . . . . . . . . . . . 17
β’ (ππΉ(πΉβπ) β π β dom πΉ) |
24 | 23 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((ππΉ(πΉβπ) β§ πππ) β π β dom πΉ) |
25 | 24 | pm4.71ri 562 |
. . . . . . . . . . . . . . 15
β’ ((ππΉ(πΉβπ) β§ πππ) β (π β dom πΉ β§ (ππΉ(πΉβπ) β§ πππ))) |
26 | 20, 25 | bitri 275 |
. . . . . . . . . . . . . 14
β’ ((πππ β§ ππΉ(πΉβπ)) β (π β dom πΉ β§ (ππΉ(πΉβπ) β§ πππ))) |
27 | 26 | exbii 1851 |
. . . . . . . . . . . . 13
β’
(βπ(πππ β§ ππΉ(πΉβπ)) β βπ(π β dom πΉ β§ (ππΉ(πΉβπ) β§ πππ))) |
28 | | vex 3450 |
. . . . . . . . . . . . . 14
β’ π β V |
29 | 28, 22 | brco 5827 |
. . . . . . . . . . . . 13
β’ (π(πΉ β π)(πΉβπ) β βπ(πππ β§ ππΉ(πΉβπ))) |
30 | | df-rex 3075 |
. . . . . . . . . . . . 13
β’
(βπ β dom
πΉ(ππΉ(πΉβπ) β§ πππ) β βπ(π β dom πΉ β§ (ππΉ(πΉβπ) β§ πππ))) |
31 | 27, 29, 30 | 3bitr4i 303 |
. . . . . . . . . . . 12
β’ (π(πΉ β π)(πΉβπ) β βπ β dom πΉ(ππΉ(πΉβπ) β§ πππ)) |
32 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π β π β§ π β π)) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β πΉ Fn π) |
33 | | fnbrfvb 6896 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ Fn π β§ π β π) β ((πΉβπ) = (πΉβπ) β ππΉ(πΉβπ))) |
34 | 32, 33 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π β π β§ π β π)) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β§ π β π) β ((πΉβπ) = (πΉβπ) β ππΉ(πΉβπ))) |
35 | 34 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π β§ π β π)) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β§ π β π) β (((πΉβπ) = (πΉβπ) β§ πππ) β (ππΉ(πΉβπ) β§ πππ))) |
36 | | imasleval.e |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πππ β πππ))) |
37 | 36 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πππ β πππ))) |
38 | 37 | an32s 651 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πππ β πππ))) |
39 | 38 | anassrs 469 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π β π β§ π β π)) β§ π β π) β§ π β π) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πππ β πππ))) |
40 | 39 | impl 457 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π β π β§ π β π)) β§ π β π) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β§ (πΉβπ) = (πΉβπ)) β (πππ β πππ)) |
41 | 40 | pm5.32da 580 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π β π β§ π β π)) β§ π β π) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β (((πΉβπ) = (πΉβπ) β§ πππ) β ((πΉβπ) = (πΉβπ) β§ πππ))) |
42 | 41 | an32s 651 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π β§ π β π)) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β§ π β π) β (((πΉβπ) = (πΉβπ) β§ πππ) β ((πΉβπ) = (πΉβπ) β§ πππ))) |
43 | 35, 42 | bitr3d 281 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π β§ π β π)) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β§ π β π) β ((ππΉ(πΉβπ) β§ πππ) β ((πΉβπ) = (πΉβπ) β§ πππ))) |
44 | 43 | rexbidva 3174 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β π β§ π β π)) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β (βπ β π (ππΉ(πΉβπ) β§ πππ) β βπ β π ((πΉβπ) = (πΉβπ) β§ πππ))) |
45 | | r19.41v 3186 |
. . . . . . . . . . . . . 14
β’
(βπ β
π ((πΉβπ) = (πΉβπ) β§ πππ) β (βπ β π (πΉβπ) = (πΉβπ) β§ πππ)) |
46 | 44, 45 | bitrdi 287 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β π β§ π β π)) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β (βπ β π (ππΉ(πΉβπ) β§ πππ) β (βπ β π (πΉβπ) = (πΉβπ) β§ πππ))) |
47 | 15 | rexeqdv 3315 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π β π)) β (βπ β dom πΉ(ππΉ(πΉβπ) β§ πππ) β βπ β π (ππΉ(πΉβπ) β§ πππ))) |
48 | 47 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β π β§ π β π)) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β (βπ β dom πΉ(ππΉ(πΉβπ) β§ πππ) β βπ β π (ππΉ(πΉβπ) β§ πππ))) |
49 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π β§ π β π)) β π β π) |
50 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ (πΉβπ) = (πΉβπ) |
51 | | fveqeq2 6852 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((πΉβπ) = (πΉβπ) β (πΉβπ) = (πΉβπ))) |
52 | 51 | rspcev 3582 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ (πΉβπ) = (πΉβπ)) β βπ β π (πΉβπ) = (πΉβπ)) |
53 | 49, 50, 52 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π β π)) β βπ β π (πΉβπ) = (πΉβπ)) |
54 | 53 | biantrurd 534 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π β π)) β (πππ β (βπ β π (πΉβπ) = (πΉβπ) β§ πππ))) |
55 | 54 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β π β§ π β π)) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β (πππ β (βπ β π (πΉβπ) = (πΉβπ) β§ πππ))) |
56 | 46, 48, 55 | 3bitr4d 311 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β π β§ π β π)) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β (βπ β dom πΉ(ππΉ(πΉβπ) β§ πππ) β πππ)) |
57 | 31, 56 | bitrid 283 |
. . . . . . . . . . 11
β’ ((((π β§ (π β π β§ π β π)) β§ π β π) β§ (πΉβπ) = (πΉβπ)) β (π(πΉ β π)(πΉβπ) β πππ)) |
58 | 57 | pm5.32da 580 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β (((πΉβπ) = (πΉβπ) β§ π(πΉ β π)(πΉβπ)) β ((πΉβπ) = (πΉβπ) β§ πππ))) |
59 | 19, 58 | bitr3d 281 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β ((ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)) β ((πΉβπ) = (πΉβπ) β§ πππ))) |
60 | 59 | rexbidva 3174 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β (βπ β π (ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)) β βπ β π ((πΉβπ) = (πΉβπ) β§ πππ))) |
61 | 16, 60 | bitrd 279 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β (βπ β dom πΉ(ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)) β βπ β π ((πΉβπ) = (πΉβπ) β§ πππ))) |
62 | | fvex 6856 |
. . . . . . . . . . . 12
β’ (πΉβπ) β V |
63 | 62, 28 | brcnv 5839 |
. . . . . . . . . . 11
β’ ((πΉβπ)β‘πΉπ β ππΉ(πΉβπ)) |
64 | 63 | anbi1i 625 |
. . . . . . . . . 10
β’ (((πΉβπ)β‘πΉπ β§ π(πΉ β π)(πΉβπ)) β (ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ))) |
65 | 28, 62 | breldm 5865 |
. . . . . . . . . . . 12
β’ (ππΉ(πΉβπ) β π β dom πΉ) |
66 | 65 | adantr 482 |
. . . . . . . . . . 11
β’ ((ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)) β π β dom πΉ) |
67 | 66 | pm4.71ri 562 |
. . . . . . . . . 10
β’ ((ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)) β (π β dom πΉ β§ (ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)))) |
68 | 64, 67 | bitri 275 |
. . . . . . . . 9
β’ (((πΉβπ)β‘πΉπ β§ π(πΉ β π)(πΉβπ)) β (π β dom πΉ β§ (ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)))) |
69 | 68 | exbii 1851 |
. . . . . . . 8
β’
(βπ((πΉβπ)β‘πΉπ β§ π(πΉ β π)(πΉβπ)) β βπ(π β dom πΉ β§ (ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)))) |
70 | 62, 22 | brco 5827 |
. . . . . . . 8
β’ ((πΉβπ)((πΉ β π) β β‘πΉ)(πΉβπ) β βπ((πΉβπ)β‘πΉπ β§ π(πΉ β π)(πΉβπ))) |
71 | | df-rex 3075 |
. . . . . . . 8
β’
(βπ β dom
πΉ(ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)) β βπ(π β dom πΉ β§ (ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)))) |
72 | 69, 70, 71 | 3bitr4ri 304 |
. . . . . . 7
β’
(βπ β dom
πΉ(ππΉ(πΉβπ) β§ π(πΉ β π)(πΉβπ)) β (πΉβπ)((πΉ β π) β β‘πΉ)(πΉβπ)) |
73 | | r19.41v 3186 |
. . . . . . 7
β’
(βπ β
π ((πΉβπ) = (πΉβπ) β§ πππ) β (βπ β π (πΉβπ) = (πΉβπ) β§ πππ)) |
74 | 61, 72, 73 | 3bitr3g 313 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β ((πΉβπ)((πΉ β π) β β‘πΉ)(πΉβπ) β (βπ β π (πΉβπ) = (πΉβπ) β§ πππ))) |
75 | | imasless.u |
. . . . . . . . 9
β’ (π β π = (πΉ βs π
)) |
76 | | imasless.v |
. . . . . . . . 9
β’ (π β π = (Baseβπ
)) |
77 | | imasless.r |
. . . . . . . . 9
β’ (π β π
β π) |
78 | | imasleval.n |
. . . . . . . . 9
β’ π = (leβπ
) |
79 | | imasless.l |
. . . . . . . . 9
β’ β€ =
(leβπ) |
80 | 75, 76, 11, 77, 78, 79 | imasle 17406 |
. . . . . . . 8
β’ (π β β€ = ((πΉ β π) β β‘πΉ)) |
81 | 80 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β β€ = ((πΉ β π) β β‘πΉ)) |
82 | 81 | breqd 5117 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β ((πΉβπ) β€ (πΉβπ) β (πΉβπ)((πΉ β π) β β‘πΉ)(πΉβπ))) |
83 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β π β π) |
84 | | eqid 2737 |
. . . . . . . 8
β’ (πΉβπ) = (πΉβπ) |
85 | | fveqeq2 6852 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ) = (πΉβπ) β (πΉβπ) = (πΉβπ))) |
86 | 85 | rspcev 3582 |
. . . . . . . 8
β’ ((π β π β§ (πΉβπ) = (πΉβπ)) β βπ β π (πΉβπ) = (πΉβπ)) |
87 | 83, 84, 86 | sylancl 587 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β βπ β π (πΉβπ) = (πΉβπ)) |
88 | 87 | biantrurd 534 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β (πππ β (βπ β π (πΉβπ) = (πΉβπ) β§ πππ))) |
89 | 74, 82, 88 | 3bitr4d 311 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β ((πΉβπ) β€ (πΉβπ) β πππ)) |
90 | 89 | expcom 415 |
. . . 4
β’ ((π β π β§ π β π) β (π β ((πΉβπ) β€ (πΉβπ) β πππ))) |
91 | 5, 10, 90 | vtocl2ga 3536 |
. . 3
β’ ((π β π β§ π β π) β (π β ((πΉβπ) β€ (πΉβπ) β πππ))) |
92 | 91 | com12 32 |
. 2
β’ (π β ((π β π β§ π β π) β ((πΉβπ) β€ (πΉβπ) β πππ))) |
93 | 92 | 3impib 1117 |
1
β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β€ (πΉβπ) β πππ)) |