Step | Hyp | Ref
| Expression |
1 | | ctinfom 12396 |
. . . 4
DECID
|
2 | 1 | simplbi 274 |
. . 3
DECID
|
3 | 1 | simprbi 275 |
. . . 4
|
4 | | simpl 109 |
. . . . . 6
|
5 | 4 | a1i 9 |
. . . . 5
|
6 | 5 | eximdv 1878 |
. . . 4
|
7 | 3, 6 | mpd 13 |
. . 3
|
8 | | nnenom 10404 |
. . . . . 6
|
9 | | entr 6774 |
. . . . . 6
|
10 | 8, 9 | mpan2 425 |
. . . . 5
|
11 | 10 | ensymd 6773 |
. . . 4
|
12 | | endom 6753 |
. . . 4
|
13 | 11, 12 | syl 14 |
. . 3
|
14 | 2, 7, 13 | 3jca 1177 |
. 2
DECID
|
15 | | simp1 997 |
. . 3
DECID
DECID |
16 | | 3simpb 995 |
. . . 4
DECID
DECID |
17 | | simp2 998 |
. . . 4
DECID
|
18 | | simp2 998 |
. . . . . . . 8
DECID
|
19 | | simpl1 1000 |
. . . . . . . . . . . 12
DECID
DECID
|
20 | | equequ1 1710 |
. . . . . . . . . . . . . . 15
|
21 | 20 | dcbid 838 |
. . . . . . . . . . . . . 14
DECID
DECID
|
22 | 21 | ralbidv 2475 |
. . . . . . . . . . . . 13
DECID
DECID |
23 | 22 | cbvralv 2701 |
. . . . . . . . . . . 12
DECID
DECID |
24 | 19, 23 | sylib 122 |
. . . . . . . . . . 11
DECID
DECID
|
25 | | simpl3 1002 |
. . . . . . . . . . 11
DECID |
26 | | fof 5430 |
. . . . . . . . . . . . . 14
|
27 | | imassrn 4974 |
. . . . . . . . . . . . . . 15
|
28 | | frn 5366 |
. . . . . . . . . . . . . . 15
|
29 | 27, 28 | sstrid 3164 |
. . . . . . . . . . . . . 14
|
30 | 26, 29 | syl 14 |
. . . . . . . . . . . . 13
|
31 | 30 | ad2antrr 488 |
. . . . . . . . . . . 12
|
32 | 31 | 3adantl1 1153 |
. . . . . . . . . . 11
DECID |
33 | | simpl2 1001 |
. . . . . . . . . . . . 13
DECID |
34 | | equequ1 1710 |
. . . . . . . . . . . . . . . 16
|
35 | 34 | dcbid 838 |
. . . . . . . . . . . . . . 15
DECID
DECID
|
36 | | equequ2 1711 |
. . . . . . . . . . . . . . . 16
|
37 | 36 | dcbid 838 |
. . . . . . . . . . . . . . 15
DECID
DECID
|
38 | 35, 37 | cbvral2v 2714 |
. . . . . . . . . . . . . 14
DECID
DECID |
39 | | ssralv 3217 |
. . . . . . . . . . . . . . . . 17
DECID
DECID |
40 | 30, 39 | syl 14 |
. . . . . . . . . . . . . . . 16
DECID
DECID |
41 | 40 | ralimdv 2543 |
. . . . . . . . . . . . . . 15
DECID
DECID |
42 | | ssralv 3217 |
. . . . . . . . . . . . . . 15
DECID DECID |
43 | 30, 41, 42 | sylsyld 58 |
. . . . . . . . . . . . . 14
DECID
DECID |
44 | 38, 43 | biimtrid 152 |
. . . . . . . . . . . . 13
DECID
DECID |
45 | 33, 19, 44 | sylc 62 |
. . . . . . . . . . . 12
DECID DECID |
46 | | simpr 110 |
. . . . . . . . . . . . . 14
|
47 | | fofun 5431 |
. . . . . . . . . . . . . . . . 17
|
48 | 47 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
|
49 | | ordom 4600 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | ordtr 4372 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
|
52 | | trss 4105 |
. . . . . . . . . . . . . . . . . 18
|
53 | 51, 46, 52 | mpsyl 65 |
. . . . . . . . . . . . . . . . 17
|
54 | 26 | fdmd 5364 |
. . . . . . . . . . . . . . . . . 18
|
55 | 54 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
|
56 | 53, 55 | sseqtrrd 3192 |
. . . . . . . . . . . . . . . 16
|
57 | | fores 5439 |
. . . . . . . . . . . . . . . 16
|
58 | 48, 56, 57 | syl2anc 411 |
. . . . . . . . . . . . . . 15
|
59 | | vex 2738 |
. . . . . . . . . . . . . . . . 17
|
60 | 59 | resex 4941 |
. . . . . . . . . . . . . . . 16
|
61 | | foeq1 5426 |
. . . . . . . . . . . . . . . 16
|
62 | 60, 61 | spcev 2830 |
. . . . . . . . . . . . . . 15
|
63 | 58, 62 | syl 14 |
. . . . . . . . . . . . . 14
|
64 | | foeq2 5427 |
. . . . . . . . . . . . . . . 16
|
65 | 64 | exbidv 1823 |
. . . . . . . . . . . . . . 15
|
66 | 65 | rspcev 2839 |
. . . . . . . . . . . . . 14
|
67 | 46, 63, 66 | syl2anc 411 |
. . . . . . . . . . . . 13
|
68 | 67 | 3adantl1 1153 |
. . . . . . . . . . . 12
DECID |
69 | | fidcenum 6945 |
. . . . . . . . . . . 12
DECID |
70 | 45, 68, 69 | sylanbrc 417 |
. . . . . . . . . . 11
DECID |
71 | 24, 25, 32, 70 | inffinp1 12397 |
. . . . . . . . . 10
DECID
|
72 | | simprl 529 |
. . . . . . . . . . . 12
DECID
|
73 | | foelrn 5744 |
. . . . . . . . . . . 12
|
74 | 33, 72, 73 | syl2an2r 595 |
. . . . . . . . . . 11
DECID
|
75 | | simpr 110 |
. . . . . . . . . . . . . 14
DECID
|
76 | | simprr 531 |
. . . . . . . . . . . . . . 15
DECID
|
77 | 76 | ad2antrr 488 |
. . . . . . . . . . . . . 14
DECID
|
78 | 75, 77 | eqneltrrd 2272 |
. . . . . . . . . . . . 13
DECID
|
79 | 78 | ex 115 |
. . . . . . . . . . . 12
DECID
|
80 | 79 | reximdva 2577 |
. . . . . . . . . . 11
DECID
|
81 | 74, 80 | mpd 13 |
. . . . . . . . . 10
DECID
|
82 | 71, 81 | rexlimddv 2597 |
. . . . . . . . 9
DECID |
83 | 82 | ralrimiva 2548 |
. . . . . . . 8
DECID
|
84 | 18, 83 | jca 306 |
. . . . . . 7
DECID
|
85 | 84 | 3com23 1209 |
. . . . . 6
DECID
|
86 | 85 | 3expia 1205 |
. . . . 5
DECID
|
87 | 86 | eximdv 1878 |
. . . 4
DECID
|
88 | 16, 17, 87 | sylc 62 |
. . 3
DECID
|
89 | 15, 88, 1 | sylanbrc 417 |
. 2
DECID
|
90 | 14, 89 | impbii 126 |
1
DECID
|