Step | Hyp | Ref
| Expression |
1 | | 2ndctop 21250 |
. 2
|
2 | | is2ndc 21249 |
. . . 4
|
3 | | ssrab2 3687 |
. . . . . . . . . . 11
|
4 | | bastg 20770 |
. . . . . . . . . . . 12
|
5 | 4 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
6 | 3, 5 | syl5ss 3614 |
. . . . . . . . . 10
|
7 | | fvex 6201 |
. . . . . . . . . . 11
|
8 | 7 | elpw2 4828 |
. . . . . . . . . 10
|
9 | 6, 8 | sylibr 224 |
. . . . . . . . 9
|
10 | | vex 3203 |
. . . . . . . . . . 11
|
11 | | ssdomg 8001 |
. . . . . . . . . . 11
|
12 | 10, 3, 11 | mp2 9 |
. . . . . . . . . 10
|
13 | | simp2 1062 |
. . . . . . . . . 10
|
14 | | domtr 8009 |
. . . . . . . . . 10
|
15 | 12, 13, 14 | sylancr 695 |
. . . . . . . . 9
|
16 | | eltg2b 20763 |
. . . . . . . . . . . 12
|
17 | 16 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
18 | | elequ1 1997 |
. . . . . . . . . . . . . . 15
|
19 | 18 | anbi1d 741 |
. . . . . . . . . . . . . 14
|
20 | 19 | rexbidv 3052 |
. . . . . . . . . . . . 13
|
21 | 20 | rspccv 3306 |
. . . . . . . . . . . 12
|
22 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
23 | 22 | adantrr 753 |
. . . . . . . . . . . . . . . 16
|
24 | | elequ2 2004 |
. . . . . . . . . . . . . . . . 17
|
25 | 24 | elrab 3363 |
. . . . . . . . . . . . . . . 16
|
26 | 23, 25 | sylibr 224 |
. . . . . . . . . . . . . . 15
|
27 | 26 | adantl 482 |
. . . . . . . . . . . . . 14
|
28 | | simprr 796 |
. . . . . . . . . . . . . 14
|
29 | | elequ2 2004 |
. . . . . . . . . . . . . . . 16
|
30 | | sseq1 3626 |
. . . . . . . . . . . . . . . 16
|
31 | 29, 30 | anbi12d 747 |
. . . . . . . . . . . . . . 15
|
32 | 31 | rspcev 3309 |
. . . . . . . . . . . . . 14
|
33 | 27, 28, 32 | syl2anc 693 |
. . . . . . . . . . . . 13
|
34 | 33 | rexlimdvaa 3032 |
. . . . . . . . . . . 12
|
35 | 21, 34 | syl9r 78 |
. . . . . . . . . . 11
|
36 | 17, 35 | sylbid 230 |
. . . . . . . . . 10
|
37 | 36 | ralrimiv 2965 |
. . . . . . . . 9
|
38 | | breq1 4656 |
. . . . . . . . . . 11
|
39 | | rexeq 3139 |
. . . . . . . . . . . . 13
|
40 | 39 | imbi2d 330 |
. . . . . . . . . . . 12
|
41 | 40 | ralbidv 2986 |
. . . . . . . . . . 11
|
42 | 38, 41 | anbi12d 747 |
. . . . . . . . . 10
|
43 | 42 | rspcev 3309 |
. . . . . . . . 9
|
44 | 9, 15, 37, 43 | syl12anc 1324 |
. . . . . . . 8
|
45 | 44 | 3expia 1267 |
. . . . . . 7
|
46 | | unieq 4444 |
. . . . . . . . 9
|
47 | 46 | eleq2d 2687 |
. . . . . . . 8
|
48 | | pweq 4161 |
. . . . . . . . 9
|
49 | | raleq 3138 |
. . . . . . . . . 10
|
50 | 49 | anbi2d 740 |
. . . . . . . . 9
|
51 | 48, 50 | rexeqbidv 3153 |
. . . . . . . 8
|
52 | 47, 51 | imbi12d 334 |
. . . . . . 7
|
53 | 45, 52 | syl5ibcom 235 |
. . . . . 6
|
54 | 53 | expimpd 629 |
. . . . 5
|
55 | 54 | rexlimiv 3027 |
. . . 4
|
56 | 2, 55 | sylbi 207 |
. . 3
|
57 | 56 | ralrimiv 2965 |
. 2
|
58 | | eqid 2622 |
. . 3
|
59 | 58 | is1stc2 21245 |
. 2
|
60 | 1, 57, 59 | sylanbrc 698 |
1
|