Proof of Theorem iscatd
Step | Hyp | Ref
| Expression |
1 | | iscatd.1 |
. . . . . 6
|
2 | | iscatd.2 |
. . . . . . . . . . 11
|
3 | 2 | 3exp2 1285 |
. . . . . . . . . 10
|
4 | 3 | imp31 448 |
. . . . . . . . 9
|
5 | 4 | ralrimiv 2965 |
. . . . . . . 8
|
6 | | iscatd.3 |
. . . . . . . . . . 11
|
7 | 6 | 3exp2 1285 |
. . . . . . . . . 10
|
8 | 7 | imp31 448 |
. . . . . . . . 9
|
9 | 8 | ralrimiv 2965 |
. . . . . . . 8
|
10 | 5, 9 | jca 554 |
. . . . . . 7
|
11 | 10 | ralrimiva 2966 |
. . . . . 6
|
12 | | oveq1 6657 |
. . . . . . . . . . 11
|
13 | 12 | eqeq1d 2624 |
. . . . . . . . . 10
|
14 | 13 | ralbidv 2986 |
. . . . . . . . 9
|
15 | | oveq2 6658 |
. . . . . . . . . . 11
|
16 | 15 | eqeq1d 2624 |
. . . . . . . . . 10
|
17 | 16 | ralbidv 2986 |
. . . . . . . . 9
|
18 | 14, 17 | anbi12d 747 |
. . . . . . . 8
|
19 | 18 | ralbidv 2986 |
. . . . . . 7
|
20 | 19 | rspcev 3309 |
. . . . . 6
|
21 | 1, 11, 20 | syl2anc 693 |
. . . . 5
|
22 | | iscatd.4 |
. . . . . . . . . . 11
|
23 | 22 | 3expia 1267 |
. . . . . . . . . 10
|
24 | 23 | 3exp2 1285 |
. . . . . . . . 9
|
25 | 24 | imp43 621 |
. . . . . . . 8
|
26 | | iscatd.5 |
. . . . . . . . . . . . . . . . . 18
|
27 | 26 | 3expa 1265 |
. . . . . . . . . . . . . . . . 17
|
28 | 27 | 3exp2 1285 |
. . . . . . . . . . . . . . . 16
|
29 | 28 | imp32 449 |
. . . . . . . . . . . . . . 15
|
30 | 29 | ralrimiv 2965 |
. . . . . . . . . . . . . 14
|
31 | 30 | ex 450 |
. . . . . . . . . . . . 13
|
32 | 31 | expr 643 |
. . . . . . . . . . . 12
|
33 | 32 | expd 452 |
. . . . . . . . . . 11
|
34 | 33 | expr 643 |
. . . . . . . . . 10
|
35 | 34 | imp42 620 |
. . . . . . . . 9
|
36 | 35 | ralrimdva 2969 |
. . . . . . . 8
|
37 | 25, 36 | jcad 555 |
. . . . . . 7
|
38 | 37 | ralrimivv 2970 |
. . . . . 6
|
39 | 38 | ralrimivva 2971 |
. . . . 5
|
40 | 21, 39 | jca 554 |
. . . 4
|
41 | 40 | ralrimiva 2966 |
. . 3
|
42 | | iscatd.b |
. . . 4
|
43 | | iscatd.h |
. . . . . . 7
|
44 | 43 | oveqd 6667 |
. . . . . 6
|
45 | 43 | oveqd 6667 |
. . . . . . . . 9
|
46 | | iscatd.o |
. . . . . . . . . . . 12
comp |
47 | 46 | oveqd 6667 |
. . . . . . . . . . 11
comp |
48 | 47 | oveqd 6667 |
. . . . . . . . . 10
comp |
49 | 48 | eqeq1d 2624 |
. . . . . . . . 9
comp |
50 | 45, 49 | raleqbidv 3152 |
. . . . . . . 8
comp |
51 | 43 | oveqd 6667 |
. . . . . . . . 9
|
52 | 46 | oveqd 6667 |
. . . . . . . . . . 11
comp |
53 | 52 | oveqd 6667 |
. . . . . . . . . 10
comp |
54 | 53 | eqeq1d 2624 |
. . . . . . . . 9
comp |
55 | 51, 54 | raleqbidv 3152 |
. . . . . . . 8
comp |
56 | 50, 55 | anbi12d 747 |
. . . . . . 7
comp comp |
57 | 42, 56 | raleqbidv 3152 |
. . . . . 6
comp comp |
58 | 44, 57 | rexeqbidv 3153 |
. . . . 5
comp
comp |
59 | 43 | oveqd 6667 |
. . . . . . . . 9
|
60 | 46 | oveqd 6667 |
. . . . . . . . . . . 12
comp |
61 | 60 | oveqd 6667 |
. . . . . . . . . . 11
comp |
62 | 43 | oveqd 6667 |
. . . . . . . . . . 11
|
63 | 61, 62 | eleq12d 2695 |
. . . . . . . . . 10
comp |
64 | 43 | oveqd 6667 |
. . . . . . . . . . . 12
|
65 | 46 | oveqd 6667 |
. . . . . . . . . . . . . 14
comp |
66 | 46 | oveqd 6667 |
. . . . . . . . . . . . . . 15
comp |
67 | 66 | oveqd 6667 |
. . . . . . . . . . . . . 14
comp |
68 | | eqidd 2623 |
. . . . . . . . . . . . . 14
|
69 | 65, 67, 68 | oveq123d 6671 |
. . . . . . . . . . . . 13
comp comp |
70 | 46 | oveqd 6667 |
. . . . . . . . . . . . . 14
comp |
71 | | eqidd 2623 |
. . . . . . . . . . . . . 14
|
72 | 70, 71, 61 | oveq123d 6671 |
. . . . . . . . . . . . 13
comp comp |
73 | 69, 72 | eqeq12d 2637 |
. . . . . . . . . . . 12
comp comp comp comp |
74 | 64, 73 | raleqbidv 3152 |
. . . . . . . . . . 11
comp comp comp comp |
75 | 42, 74 | raleqbidv 3152 |
. . . . . . . . . 10
comp comp comp comp |
76 | 63, 75 | anbi12d 747 |
. . . . . . . . 9
comp
comp comp comp comp |
77 | 59, 76 | raleqbidv 3152 |
. . . . . . . 8
comp
comp comp comp comp |
78 | 51, 77 | raleqbidv 3152 |
. . . . . . 7
comp comp comp comp comp |
79 | 42, 78 | raleqbidv 3152 |
. . . . . 6
comp comp comp comp comp |
80 | 42, 79 | raleqbidv 3152 |
. . . . 5
comp
comp comp comp comp |
81 | 58, 80 | anbi12d 747 |
. . . 4
comp comp comp
comp comp comp comp |
82 | 42, 81 | raleqbidv 3152 |
. . 3
comp comp comp
comp comp comp comp |
83 | 41, 82 | mpbid 222 |
. 2
comp comp comp
comp comp comp comp |
84 | | iscatd.c |
. . 3
|
85 | | eqid 2622 |
. . . 4
|
86 | | eqid 2622 |
. . . 4
|
87 | | eqid 2622 |
. . . 4
comp comp |
88 | 85, 86, 87 | iscat 16333 |
. . 3
comp comp comp
comp comp comp comp |
89 | 84, 88 | syl 17 |
. 2
comp
comp comp
comp comp comp comp |
90 | 83, 89 | mpbird 247 |
1
|