Proof of Theorem rescabs
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
↾s sSet cat
↾s sSet cat
|
2 | | ovexd 6680 |
. . . 4
↾s sSet
|
3 | | rescabs.s |
. . . . 5
|
4 | | rescabs.t |
. . . . 5
|
5 | 3, 4 | ssexd 4805 |
. . . 4
|
6 | | rescabs.j |
. . . 4
|
7 | 1, 2, 5, 6 | rescval2 16488 |
. . 3
↾s sSet
cat ↾s sSet
↾s sSet
|
8 | | simpr 477 |
. . . . . . 7
↾s ↾s
|
9 | | ovexd 6680 |
. . . . . . 7
↾s
↾s sSet |
10 | 5 | adantr 481 |
. . . . . . 7
↾s |
11 | | eqid 2622 |
. . . . . . . 8
↾s sSet
↾s ↾s sSet
↾s |
12 | | baseid 15919 |
. . . . . . . . 9
Slot |
13 | | 1re 10039 |
. . . . . . . . . . 11
|
14 | | 1nn 11031 |
. . . . . . . . . . . 12
|
15 | | 4nn0 11311 |
. . . . . . . . . . . 12
|
16 | | 1nn0 11308 |
. . . . . . . . . . . 12
|
17 | | 1lt10 11681 |
. . . . . . . . . . . 12
; |
18 | 14, 15, 16, 17 | declti 11546 |
. . . . . . . . . . 11
; |
19 | 13, 18 | ltneii 10150 |
. . . . . . . . . 10
; |
20 | | basendx 15923 |
. . . . . . . . . . 11
|
21 | | homndx 16074 |
. . . . . . . . . . 11
; |
22 | 20, 21 | neeq12i 2860 |
. . . . . . . . . 10
; |
23 | 19, 22 | mpbir 221 |
. . . . . . . . 9
|
24 | 12, 23 | setsnid 15915 |
. . . . . . . 8
↾s
↾s sSet |
25 | 11, 24 | ressid2 15928 |
. . . . . . 7
↾s ↾s sSet
↾s sSet
↾s ↾s sSet |
26 | 8, 9, 10, 25 | syl3anc 1326 |
. . . . . 6
↾s ↾s sSet
↾s ↾s sSet |
27 | 26 | oveq1d 6665 |
. . . . 5
↾s ↾s sSet
↾s sSet
↾s sSet sSet |
28 | | ovex 6678 |
. . . . . 6
↾s |
29 | | xpexg 6960 |
. . . . . . . . 9
|
30 | 5, 5, 29 | syl2anc 693 |
. . . . . . . 8
|
31 | | fnex 6481 |
. . . . . . . 8
|
32 | 6, 30, 31 | syl2anc 693 |
. . . . . . 7
|
33 | 32 | adantr 481 |
. . . . . 6
↾s |
34 | | setsabs 15902 |
. . . . . 6
↾s ↾s sSet
sSet
↾s sSet
|
35 | 28, 33, 34 | sylancr 695 |
. . . . 5
↾s ↾s sSet
sSet
↾s sSet
|
36 | | eqid 2622 |
. . . . . . . . . . . . . 14
↾s ↾s |
37 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
38 | 36, 37 | ressbas 15930 |
. . . . . . . . . . . . 13
↾s |
39 | 3, 38 | syl 17 |
. . . . . . . . . . . 12
↾s |
40 | 39 | sseq1d 3632 |
. . . . . . . . . . 11
↾s |
41 | 40 | biimpar 502 |
. . . . . . . . . 10
↾s |
42 | | inss2 3834 |
. . . . . . . . . . 11
|
43 | 42 | a1i 11 |
. . . . . . . . . 10
↾s |
44 | 41, 43 | ssind 3837 |
. . . . . . . . 9
↾s |
45 | 4 | adantr 481 |
. . . . . . . . . 10
↾s |
46 | | ssrin 3838 |
. . . . . . . . . 10
|
47 | 45, 46 | syl 17 |
. . . . . . . . 9
↾s |
48 | 44, 47 | eqssd 3620 |
. . . . . . . 8
↾s |
49 | 48 | oveq2d 6666 |
. . . . . . 7
↾s ↾s
↾s |
50 | 3 | adantr 481 |
. . . . . . . 8
↾s |
51 | 37 | ressinbas 15936 |
. . . . . . . 8
↾s ↾s |
52 | 50, 51 | syl 17 |
. . . . . . 7
↾s ↾s ↾s |
53 | 37 | ressinbas 15936 |
. . . . . . . 8
↾s ↾s |
54 | 10, 53 | syl 17 |
. . . . . . 7
↾s ↾s ↾s |
55 | 49, 52, 54 | 3eqtr4d 2666 |
. . . . . 6
↾s ↾s ↾s |
56 | 55 | oveq1d 6665 |
. . . . 5
↾s
↾s sSet
↾s sSet |
57 | 27, 35, 56 | 3eqtrd 2660 |
. . . 4
↾s ↾s sSet
↾s sSet
↾s sSet
|
58 | | simpr 477 |
. . . . . . . 8
↾s
↾s |
59 | | ovexd 6680 |
. . . . . . . 8
↾s
↾s sSet
|
60 | 5 | adantr 481 |
. . . . . . . 8
↾s
|
61 | 11, 24 | ressval2 15929 |
. . . . . . . 8
↾s ↾s sSet
↾s sSet
↾s
↾s sSet sSet ↾s |
62 | 58, 59, 60, 61 | syl3anc 1326 |
. . . . . . 7
↾s
↾s sSet
↾s
↾s sSet sSet ↾s |
63 | | ovexd 6680 |
. . . . . . . 8
↾s
↾s |
64 | 23 | necomi 2848 |
. . . . . . . . 9
|
65 | 64 | a1i 11 |
. . . . . . . 8
↾s
|
66 | | rescabs.h |
. . . . . . . . . 10
|
67 | | xpexg 6960 |
. . . . . . . . . . 11
|
68 | 3, 3, 67 | syl2anc 693 |
. . . . . . . . . 10
|
69 | | fnex 6481 |
. . . . . . . . . 10
|
70 | 66, 68, 69 | syl2anc 693 |
. . . . . . . . 9
|
71 | 70 | adantr 481 |
. . . . . . . 8
↾s
|
72 | | fvex 6201 |
. . . . . . . . . 10
↾s |
73 | 72 | inex2 4800 |
. . . . . . . . 9
↾s |
74 | 73 | a1i 11 |
. . . . . . . 8
↾s
↾s |
75 | | fvex 6201 |
. . . . . . . . 9
|
76 | | fvex 6201 |
. . . . . . . . 9
|
77 | 75, 76 | setscom 15903 |
. . . . . . . 8
↾s
↾s ↾s sSet sSet ↾s ↾s sSet ↾s sSet
|
78 | 63, 65, 71, 74, 77 | syl22anc 1327 |
. . . . . . 7
↾s
↾s sSet
sSet
↾s
↾s sSet
↾s
sSet |
79 | | eqid 2622 |
. . . . . . . . . . 11
↾s
↾s
↾s
↾s |
80 | | eqid 2622 |
. . . . . . . . . . 11
↾s ↾s |
81 | 79, 80 | ressval2 15929 |
. . . . . . . . . 10
↾s ↾s
↾s
↾s
↾s sSet ↾s |
82 | 58, 63, 60, 81 | syl3anc 1326 |
. . . . . . . . 9
↾s
↾s ↾s ↾s sSet ↾s |
83 | 3 | adantr 481 |
. . . . . . . . . 10
↾s
|
84 | 4 | adantr 481 |
. . . . . . . . . 10
↾s
|
85 | | ressabs 15939 |
. . . . . . . . . 10
↾s ↾s ↾s |
86 | 83, 84, 85 | syl2anc 693 |
. . . . . . . . 9
↾s
↾s ↾s ↾s |
87 | 82, 86 | eqtr3d 2658 |
. . . . . . . 8
↾s
↾s sSet
↾s
↾s |
88 | 87 | oveq1d 6665 |
. . . . . . 7
↾s
↾s sSet
↾s
sSet ↾s sSet |
89 | 62, 78, 88 | 3eqtrd 2660 |
. . . . . 6
↾s
↾s sSet
↾s ↾s sSet |
90 | 89 | oveq1d 6665 |
. . . . 5
↾s
↾s sSet
↾s sSet ↾s sSet
sSet
|
91 | | ovex 6678 |
. . . . . 6
↾s |
92 | 32 | adantr 481 |
. . . . . 6
↾s
|
93 | | setsabs 15902 |
. . . . . 6
↾s ↾s sSet
sSet
↾s sSet
|
94 | 91, 92, 93 | sylancr 695 |
. . . . 5
↾s
↾s sSet
sSet
↾s sSet
|
95 | 90, 94 | eqtrd 2656 |
. . . 4
↾s
↾s sSet
↾s sSet
↾s sSet |
96 | 57, 95 | pm2.61dan 832 |
. . 3
↾s sSet
↾s sSet
↾s sSet |
97 | 7, 96 | eqtrd 2656 |
. 2
↾s sSet
cat
↾s sSet |
98 | | eqid 2622 |
. . . 4
cat cat |
99 | | rescabs.c |
. . . 4
|
100 | 98, 99, 3, 66 | rescval2 16488 |
. . 3
cat
↾s sSet
|
101 | 100 | oveq1d 6665 |
. 2
cat cat ↾s sSet
cat |
102 | | eqid 2622 |
. . 3
cat cat |
103 | 102, 99, 5, 6 | rescval2 16488 |
. 2
cat
↾s sSet
|
104 | 97, 101, 103 | 3eqtr4d 2666 |
1
cat cat cat |