Step | Hyp | Ref
| Expression |
1 | | dyadmbl.1 |
. . 3
|
2 | | dyadmbl.2 |
. . 3
|
3 | | dyadmbl.3 |
. . 3
|
4 | 1, 2, 3 | dyadmbllem 23367 |
. 2
|
5 | | isfinite 8549 |
. . . 4
|
6 | | iccf 12272 |
. . . . . 6
|
7 | | ffun 6048 |
. . . . . 6
|
8 | | funiunfv 6506 |
. . . . . 6
|
9 | 6, 7, 8 | mp2b 10 |
. . . . 5
|
10 | | simpr 477 |
. . . . . 6
|
11 | | ssrab2 3687 |
. . . . . . . . . . . . . . . 16
|
12 | 2, 11 | eqsstri 3635 |
. . . . . . . . . . . . . . 15
|
13 | 12, 3 | syl5ss 3614 |
. . . . . . . . . . . . . 14
|
14 | 1 | dyadf 23359 |
. . . . . . . . . . . . . . . 16
|
15 | | frn 6053 |
. . . . . . . . . . . . . . . 16
|
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
17 | | inss2 3834 |
. . . . . . . . . . . . . . 15
|
18 | 16, 17 | sstri 3612 |
. . . . . . . . . . . . . 14
|
19 | 13, 18 | syl6ss 3615 |
. . . . . . . . . . . . 13
|
20 | 19 | adantr 481 |
. . . . . . . . . . . 12
|
21 | 20 | sselda 3603 |
. . . . . . . . . . 11
|
22 | | 1st2nd2 7205 |
. . . . . . . . . . 11
|
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
|
24 | 23 | fveq2d 6195 |
. . . . . . . . 9
|
25 | | df-ov 6653 |
. . . . . . . . 9
|
26 | 24, 25 | syl6eqr 2674 |
. . . . . . . 8
|
27 | | xp1st 7198 |
. . . . . . . . . 10
|
28 | 21, 27 | syl 17 |
. . . . . . . . 9
|
29 | | xp2nd 7199 |
. . . . . . . . . 10
|
30 | 21, 29 | syl 17 |
. . . . . . . . 9
|
31 | | iccmbl 23334 |
. . . . . . . . 9
|
32 | 28, 30, 31 | syl2anc 693 |
. . . . . . . 8
|
33 | 26, 32 | eqeltrd 2701 |
. . . . . . 7
|
34 | 33 | ralrimiva 2966 |
. . . . . 6
|
35 | | finiunmbl 23312 |
. . . . . 6
|
36 | 10, 34, 35 | syl2anc 693 |
. . . . 5
|
37 | 9, 36 | syl5eqelr 2706 |
. . . 4
|
38 | 5, 37 | sylan2br 493 |
. . 3
|
39 | | nnenom 12779 |
. . . . . . 7
|
40 | | ensym 8005 |
. . . . . . 7
|
41 | | entr 8008 |
. . . . . . 7
|
42 | 39, 40, 41 | sylancr 695 |
. . . . . 6
|
43 | | bren 7964 |
. . . . . 6
|
44 | 42, 43 | sylib 208 |
. . . . 5
|
45 | | rnco2 5642 |
. . . . . . . . . 10
|
46 | | f1ofo 6144 |
. . . . . . . . . . . . 13
|
47 | 46 | adantl 482 |
. . . . . . . . . . . 12
|
48 | | forn 6118 |
. . . . . . . . . . . 12
|
49 | 47, 48 | syl 17 |
. . . . . . . . . . 11
|
50 | 49 | imaeq2d 5466 |
. . . . . . . . . 10
|
51 | 45, 50 | syl5eq 2668 |
. . . . . . . . 9
|
52 | 51 | unieqd 4446 |
. . . . . . . 8
|
53 | | f1of 6137 |
. . . . . . . . . 10
|
54 | 13, 16 | syl6ss 3615 |
. . . . . . . . . 10
|
55 | | fss 6056 |
. . . . . . . . . 10
|
56 | 53, 54, 55 | syl2anr 495 |
. . . . . . . . 9
|
57 | | fss 6056 |
. . . . . . . . . . . . . . 15
|
58 | 53, 13, 57 | syl2anr 495 |
. . . . . . . . . . . . . 14
|
59 | | simpl 473 |
. . . . . . . . . . . . . 14
|
60 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
|
61 | 58, 59, 60 | syl2an 494 |
. . . . . . . . . . . . 13
|
62 | | simpr 477 |
. . . . . . . . . . . . . 14
|
63 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
|
64 | 58, 62, 63 | syl2an 494 |
. . . . . . . . . . . . 13
|
65 | 1 | dyaddisj 23364 |
. . . . . . . . . . . . 13
|
66 | 61, 64, 65 | syl2anc 693 |
. . . . . . . . . . . 12
|
67 | 53 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
68 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . 17
|
69 | 67, 62, 68 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
70 | 12, 69 | sseldi 3601 |
. . . . . . . . . . . . . . 15
|
71 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . 17
|
72 | 67, 59, 71 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
73 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
74 | 73 | sseq1d 3632 |
. . . . . . . . . . . . . . . . . . . 20
|
75 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . 20
|
76 | 74, 75 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . 19
|
77 | 76 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . 18
|
78 | 77, 2 | elrab2 3366 |
. . . . . . . . . . . . . . . . 17
|
79 | 78 | simprbi 480 |
. . . . . . . . . . . . . . . 16
|
80 | 72, 79 | syl 17 |
. . . . . . . . . . . . . . 15
|
81 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
82 | 81 | sseq2d 3633 |
. . . . . . . . . . . . . . . . 17
|
83 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . 17
|
84 | 82, 83 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
85 | 84 | rspcv 3305 |
. . . . . . . . . . . . . . 15
|
86 | 70, 80, 85 | sylc 65 |
. . . . . . . . . . . . . 14
|
87 | | f1of1 6136 |
. . . . . . . . . . . . . . . . 17
|
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
89 | | f1fveq 6519 |
. . . . . . . . . . . . . . . 16
|
90 | 88, 89 | sylan 488 |
. . . . . . . . . . . . . . 15
|
91 | | orc 400 |
. . . . . . . . . . . . . . 15
|
92 | 90, 91 | syl6bi 243 |
. . . . . . . . . . . . . 14
|
93 | 86, 92 | syld 47 |
. . . . . . . . . . . . 13
|
94 | 12, 72 | sseldi 3601 |
. . . . . . . . . . . . . . 15
|
95 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
96 | 95 | sseq1d 3632 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 96, 97 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 98 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . 18
|
100 | 99, 2 | elrab2 3366 |
. . . . . . . . . . . . . . . . 17
|
101 | 100 | simprbi 480 |
. . . . . . . . . . . . . . . 16
|
102 | 69, 101 | syl 17 |
. . . . . . . . . . . . . . 15
|
103 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
104 | 103 | sseq2d 3633 |
. . . . . . . . . . . . . . . . 17
|
105 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . 18
|
106 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . 18
|
107 | 105, 106 | syl6bb 276 |
. . . . . . . . . . . . . . . . 17
|
108 | 104, 107 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
109 | 108 | rspcv 3305 |
. . . . . . . . . . . . . . 15
|
110 | 94, 102, 109 | sylc 65 |
. . . . . . . . . . . . . 14
|
111 | 110, 92 | syld 47 |
. . . . . . . . . . . . 13
|
112 | | olc 399 |
. . . . . . . . . . . . . 14
|
113 | 112 | a1i 11 |
. . . . . . . . . . . . 13
|
114 | 93, 111, 113 | 3jaod 1392 |
. . . . . . . . . . . 12
|
115 | 66, 114 | mpd 15 |
. . . . . . . . . . 11
|
116 | 115 | ralrimivva 2971 |
. . . . . . . . . 10
|
117 | | fveq2 6191 |
. . . . . . . . . . . 12
|
118 | 117 | fveq2d 6195 |
. . . . . . . . . . 11
|
119 | 118 | disjor 4634 |
. . . . . . . . . 10
Disj
|
120 | 116, 119 | sylibr 224 |
. . . . . . . . 9
Disj |
121 | | eqid 2622 |
. . . . . . . . 9
|
122 | 56, 120, 121 | uniiccmbl 23358 |
. . . . . . . 8
|
123 | 52, 122 | eqeltrrd 2702 |
. . . . . . 7
|
124 | 123 | ex 450 |
. . . . . 6
|
125 | 124 | exlimdv 1861 |
. . . . 5
|
126 | 44, 125 | syl5 34 |
. . . 4
|
127 | 126 | imp 445 |
. . 3
|
128 | | reex 10027 |
. . . . . . . . 9
|
129 | 128, 128 | xpex 6962 |
. . . . . . . 8
|
130 | 129 | inex2 4800 |
. . . . . . 7
|
131 | 130, 16 | ssexi 4803 |
. . . . . 6
|
132 | | ssdomg 8001 |
. . . . . 6
|
133 | 131, 13, 132 | mpsyl 68 |
. . . . 5
|
134 | | omelon 8543 |
. . . . . . . 8
|
135 | | znnen 14941 |
. . . . . . . . . . . 12
|
136 | 135, 39 | entri 8010 |
. . . . . . . . . . 11
|
137 | | nn0ennn 12778 |
. . . . . . . . . . . 12
|
138 | 137, 39 | entri 8010 |
. . . . . . . . . . 11
|
139 | | xpen 8123 |
. . . . . . . . . . 11
|
140 | 136, 138,
139 | mp2an 708 |
. . . . . . . . . 10
|
141 | | xpomen 8838 |
. . . . . . . . . 10
|
142 | 140, 141 | entri 8010 |
. . . . . . . . 9
|
143 | 142 | ensymi 8006 |
. . . . . . . 8
|
144 | | isnumi 8772 |
. . . . . . . 8
|
145 | 134, 143,
144 | mp2an 708 |
. . . . . . 7
|
146 | | ffn 6045 |
. . . . . . . . 9
|
147 | 14, 146 | ax-mp 5 |
. . . . . . . 8
|
148 | | dffn4 6121 |
. . . . . . . 8
|
149 | 147, 148 | mpbi 220 |
. . . . . . 7
|
150 | | fodomnum 8880 |
. . . . . . 7
|
151 | 145, 149,
150 | mp2 9 |
. . . . . 6
|
152 | | domentr 8015 |
. . . . . 6
|
153 | 151, 142,
152 | mp2an 708 |
. . . . 5
|
154 | | domtr 8009 |
. . . . 5
|
155 | 133, 153,
154 | sylancl 694 |
. . . 4
|
156 | | brdom2 7985 |
. . . 4
|
157 | 155, 156 | sylib 208 |
. . 3
|
158 | 38, 127, 157 | mpjaodan 827 |
. 2
|
159 | 4, 158 | eqeltrd 2701 |
1
|