Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
|
2 | 1 | rnmpt 5371 |
. 2
|
3 | | unieq 4444 |
. . . . . . . . . . . 12
|
4 | | uni0 4465 |
. . . . . . . . . . . 12
|
5 | 3, 4 | syl6eq 2672 |
. . . . . . . . . . 11
|
6 | 5 | adantl 482 |
. . . . . . . . . 10
[]
|
7 | | 0ex 4790 |
. . . . . . . . . . 11
|
8 | 7 | elsn2 4211 |
. . . . . . . . . 10
|
9 | 6, 8 | sylibr 224 |
. . . . . . . . 9
[]
|
10 | 9 | olcd 408 |
. . . . . . . 8
[]
|
11 | | ssrab2 3687 |
. . . . . . . . . 10
|
12 | | simpr 477 |
. . . . . . . . . . 11
[]
|
13 | | simplll 798 |
. . . . . . . . . . . 12
[]
[] |
14 | | simpllr 799 |
. . . . . . . . . . . 12
[]
|
15 | | simplr 792 |
. . . . . . . . . . . 12
[]
|
16 | | fin1a2lem9 9230 |
. . . . . . . . . . . 12
[]
|
17 | 13, 14, 15, 16 | syl3anc 1326 |
. . . . . . . . . . 11
[]
|
18 | | soss 5053 |
. . . . . . . . . . . 12
[] []
|
19 | 11, 13, 18 | mpsyl 68 |
. . . . . . . . . . 11
[]
[] |
20 | | fin1a2lem10 9231 |
. . . . . . . . . . 11
[] |
21 | 12, 17, 19, 20 | syl3anc 1326 |
. . . . . . . . . 10
[]
|
22 | 11, 21 | sseldi 3601 |
. . . . . . . . 9
[]
|
23 | 22 | orcd 407 |
. . . . . . . 8
[]
|
24 | 10, 23 | pm2.61dane 2881 |
. . . . . . 7
[]
|
25 | | eleq1 2689 |
. . . . . . . 8
|
26 | | eleq1 2689 |
. . . . . . . 8
|
27 | 25, 26 | orbi12d 746 |
. . . . . . 7
|
28 | 24, 27 | syl5ibrcom 237 |
. . . . . 6
[]
|
29 | 28 | rexlimdva 3031 |
. . . . 5
[]
|
30 | | simpr 477 |
. . . . . . . . . 10
[] |
31 | 30 | sselda 3603 |
. . . . . . . . 9
[]
|
32 | | ficardom 8787 |
. . . . . . . . 9
|
33 | 31, 32 | syl 17 |
. . . . . . . 8
[]
|
34 | | simpr 477 |
. . . . . . . . . . 11
[]
|
35 | | ficardid 8788 |
. . . . . . . . . . . . 13
|
36 | 31, 35 | syl 17 |
. . . . . . . . . . . 12
[]
|
37 | | ensym 8005 |
. . . . . . . . . . . 12
|
38 | | endom 7982 |
. . . . . . . . . . . 12
|
39 | 36, 37, 38 | 3syl 18 |
. . . . . . . . . . 11
[]
|
40 | | breq1 4656 |
. . . . . . . . . . . 12
|
41 | 40 | elrab 3363 |
. . . . . . . . . . 11
|
42 | 34, 39, 41 | sylanbrc 698 |
. . . . . . . . . 10
[]
|
43 | | elssuni 4467 |
. . . . . . . . . 10
|
44 | 42, 43 | syl 17 |
. . . . . . . . 9
[]
|
45 | | breq1 4656 |
. . . . . . . . . . . . 13
|
46 | 45 | elrab 3363 |
. . . . . . . . . . . 12
|
47 | | simprr 796 |
. . . . . . . . . . . . . . 15
[]
|
48 | 36 | adantr 481 |
. . . . . . . . . . . . . . 15
[]
|
49 | | domentr 8015 |
. . . . . . . . . . . . . . 15
|
50 | 47, 48, 49 | syl2anc 693 |
. . . . . . . . . . . . . 14
[]
|
51 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
[]
|
52 | | simprl 794 |
. . . . . . . . . . . . . . . 16
[]
|
53 | 51, 52 | sseldd 3604 |
. . . . . . . . . . . . . . 15
[]
|
54 | 31 | adantr 481 |
. . . . . . . . . . . . . . 15
[]
|
55 | | simplll 798 |
. . . . . . . . . . . . . . . 16
[]
[] |
56 | | simplr 792 |
. . . . . . . . . . . . . . . 16
[]
|
57 | | sorpssi 6943 |
. . . . . . . . . . . . . . . 16
[]
|
58 | 55, 52, 56, 57 | syl12anc 1324 |
. . . . . . . . . . . . . . 15
[]
|
59 | | fincssdom 9145 |
. . . . . . . . . . . . . . 15
|
60 | 53, 54, 58, 59 | syl3anc 1326 |
. . . . . . . . . . . . . 14
[]
|
61 | 50, 60 | mpbid 222 |
. . . . . . . . . . . . 13
[]
|
62 | 61 | ex 450 |
. . . . . . . . . . . 12
[]
|
63 | 46, 62 | syl5bi 232 |
. . . . . . . . . . 11
[]
|
64 | 63 | ralrimiv 2965 |
. . . . . . . . . 10
[]
|
65 | | unissb 4469 |
. . . . . . . . . 10
|
66 | 64, 65 | sylibr 224 |
. . . . . . . . 9
[]
|
67 | 44, 66 | eqssd 3620 |
. . . . . . . 8
[]
|
68 | | breq2 4657 |
. . . . . . . . . . . 12
|
69 | 68 | rabbidv 3189 |
. . . . . . . . . . 11
|
70 | 69 | unieqd 4446 |
. . . . . . . . . 10
|
71 | 70 | eqeq2d 2632 |
. . . . . . . . 9
|
72 | 71 | rspcev 3309 |
. . . . . . . 8
|
73 | 33, 67, 72 | syl2anc 693 |
. . . . . . 7
[]
|
74 | 73 | ex 450 |
. . . . . 6
[]
|
75 | | velsn 4193 |
. . . . . . 7
|
76 | | peano1 7085 |
. . . . . . . . 9
|
77 | | dom0 8088 |
. . . . . . . . . . . . . . . 16
|
78 | 77 | biimpi 206 |
. . . . . . . . . . . . . . 15
|
79 | 78 | adantl 482 |
. . . . . . . . . . . . . 14
|
80 | 79 | a1i 11 |
. . . . . . . . . . . . 13
[]
|
81 | | breq1 4656 |
. . . . . . . . . . . . . 14
|
82 | 81 | elrab 3363 |
. . . . . . . . . . . . 13
|
83 | | velsn 4193 |
. . . . . . . . . . . . 13
|
84 | 80, 82, 83 | 3imtr4g 285 |
. . . . . . . . . . . 12
[]
|
85 | 84 | ssrdv 3609 |
. . . . . . . . . . 11
[]
|
86 | | uni0b 4463 |
. . . . . . . . . . 11
|
87 | 85, 86 | sylibr 224 |
. . . . . . . . . 10
[] |
88 | 87 | eqcomd 2628 |
. . . . . . . . 9
[]
|
89 | | breq2 4657 |
. . . . . . . . . . . . 13
|
90 | 89 | rabbidv 3189 |
. . . . . . . . . . . 12
|
91 | 90 | unieqd 4446 |
. . . . . . . . . . 11
|
92 | 91 | eqeq2d 2632 |
. . . . . . . . . 10
|
93 | 92 | rspcev 3309 |
. . . . . . . . 9
|
94 | 76, 88, 93 | sylancr 695 |
. . . . . . . 8
[] |
95 | | eqeq1 2626 |
. . . . . . . . 9
|
96 | 95 | rexbidv 3052 |
. . . . . . . 8
|
97 | 94, 96 | syl5ibrcom 237 |
. . . . . . 7
[]
|
98 | 75, 97 | syl5bi 232 |
. . . . . 6
[]
|
99 | 74, 98 | jaod 395 |
. . . . 5
[]
|
100 | 29, 99 | impbid 202 |
. . . 4
[]
|
101 | | elun 3753 |
. . . 4
|
102 | 100, 101 | syl6bbr 278 |
. . 3
[]
|
103 | 102 | abbi1dv 2743 |
. 2
[]
|
104 | 2, 103 | syl5eq 2668 |
1
[]
|