Step | Hyp | Ref
| Expression |
1 | | df-rcl 37965 |
. 2
|
2 | | rabab 3223 |
. . . . . . . 8
|
3 | 2 | eqcomi 2631 |
. . . . . . 7
|
4 | 3 | inteqi 4479 |
. . . . . 6
|
5 | 4 | a1i 11 |
. . . . 5
|
6 | | vex 3203 |
. . . . . . . . . . 11
|
7 | 6 | dmex 7099 |
. . . . . . . . . 10
|
8 | 6 | rnex 7100 |
. . . . . . . . . 10
|
9 | 7, 8 | unex 6956 |
. . . . . . . . 9
|
10 | | resiexg 7102 |
. . . . . . . . 9
|
11 | 9, 10 | ax-mp 5 |
. . . . . . . 8
|
12 | 11, 6 | unex 6956 |
. . . . . . 7
|
13 | 12 | a1i 11 |
. . . . . 6
|
14 | | ssun2 3777 |
. . . . . . 7
|
15 | | dmun 5331 |
. . . . . . . . . . . 12
|
16 | | dmresi 5457 |
. . . . . . . . . . . . 13
|
17 | 16 | uneq1i 3763 |
. . . . . . . . . . . 12
|
18 | | un23 3772 |
. . . . . . . . . . . . 13
|
19 | | unidm 3756 |
. . . . . . . . . . . . . 14
|
20 | 19 | uneq1i 3763 |
. . . . . . . . . . . . 13
|
21 | 18, 20 | eqtri 2644 |
. . . . . . . . . . . 12
|
22 | 15, 17, 21 | 3eqtri 2648 |
. . . . . . . . . . 11
|
23 | | rnun 5541 |
. . . . . . . . . . . 12
|
24 | | rnresi 5479 |
. . . . . . . . . . . . 13
|
25 | 24 | uneq1i 3763 |
. . . . . . . . . . . 12
|
26 | | unass 3770 |
. . . . . . . . . . . . 13
|
27 | | unidm 3756 |
. . . . . . . . . . . . . 14
|
28 | 27 | uneq2i 3764 |
. . . . . . . . . . . . 13
|
29 | 26, 28 | eqtri 2644 |
. . . . . . . . . . . 12
|
30 | 23, 25, 29 | 3eqtri 2648 |
. . . . . . . . . . 11
|
31 | 22, 30 | uneq12i 3765 |
. . . . . . . . . 10
|
32 | | unidm 3756 |
. . . . . . . . . 10
|
33 | 31, 32 | eqtri 2644 |
. . . . . . . . 9
|
34 | 33 | reseq2i 5393 |
. . . . . . . 8
|
35 | | ssun1 3776 |
. . . . . . . 8
|
36 | 34, 35 | eqsstri 3635 |
. . . . . . 7
|
37 | 14, 36 | pm3.2i 471 |
. . . . . 6
|
38 | | dmeq 5324 |
. . . . . . . . . . 11
|
39 | | rneq 5351 |
. . . . . . . . . . 11
|
40 | 38, 39 | uneq12d 3768 |
. . . . . . . . . 10
|
41 | 40 | reseq2d 5396 |
. . . . . . . . 9
|
42 | | id 22 |
. . . . . . . . 9
|
43 | 41, 42 | sseq12d 3634 |
. . . . . . . 8
|
44 | 43 | cleq2lem 37914 |
. . . . . . 7
|
45 | 44 | intminss 4503 |
. . . . . 6
|
46 | 13, 37, 45 | sylancl 694 |
. . . . 5
|
47 | 5, 46 | eqsstrd 3639 |
. . . 4
|
48 | | dmss 5323 |
. . . . . . . . . . . . . . . 16
|
49 | | rnss 5354 |
. . . . . . . . . . . . . . . 16
|
50 | | unss12 3785 |
. . . . . . . . . . . . . . . 16
|
51 | 48, 49, 50 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
52 | | dfss 3589 |
. . . . . . . . . . . . . . 15
|
53 | 51, 52 | sylib 208 |
. . . . . . . . . . . . . 14
|
54 | | incom 3805 |
. . . . . . . . . . . . . 14
|
55 | 53, 54 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
56 | 55 | reseq2d 5396 |
. . . . . . . . . . . 12
|
57 | | resres 5409 |
. . . . . . . . . . . 12
|
58 | 56, 57 | syl6eqr 2674 |
. . . . . . . . . . 11
|
59 | | resss 5422 |
. . . . . . . . . . . 12
|
60 | 59 | a1i 11 |
. . . . . . . . . . 11
|
61 | 58, 60 | eqsstrd 3639 |
. . . . . . . . . 10
|
62 | 61 | adantr 481 |
. . . . . . . . 9
|
63 | | simpr 477 |
. . . . . . . . 9
|
64 | 62, 63 | sstrd 3613 |
. . . . . . . 8
|
65 | | simpl 473 |
. . . . . . . 8
|
66 | 64, 65 | unssd 3789 |
. . . . . . 7
|
67 | 66 | ax-gen 1722 |
. . . . . 6
|
68 | 67 | a1i 11 |
. . . . 5
|
69 | | ssintab 4494 |
. . . . 5
|
70 | 68, 69 | sylibr 224 |
. . . 4
|
71 | 47, 70 | eqssd 3620 |
. . 3
|
72 | 71 | mpteq2ia 4740 |
. 2
|
73 | 1, 72 | eqtri 2644 |
1
|