Step | Hyp | Ref
| Expression |
1 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . 19
|
2 | 1 | biimpac 503 |
. . . . . . . . . . . . . . . . . 18
|
3 | | rabid 3116 |
. . . . . . . . . . . . . . . . . . 19
|
4 | 3 | simplbi2com 657 |
. . . . . . . . . . . . . . . . . 18
|
5 | 2, 4 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
6 | 5 | impancom 456 |
. . . . . . . . . . . . . . . 16
|
7 | 6 | ancrd 577 |
. . . . . . . . . . . . . . 15
|
8 | 7 | expimpd 629 |
. . . . . . . . . . . . . 14
|
9 | 8 | reximdv2 3014 |
. . . . . . . . . . . . 13
|
10 | 9 | ralimia 2950 |
. . . . . . . . . . . 12
|
11 | 3 | simplbi 476 |
. . . . . . . . . . . . . . . 16
|
12 | 6 | pm4.71rd 667 |
. . . . . . . . . . . . . . . . 17
|
13 | | df-mpt 4730 |
. . . . . . . . . . . . . . . . . . 19
|
14 | 13 | breqi 4659 |
. . . . . . . . . . . . . . . . . 18
|
15 | | df-br 4654 |
. . . . . . . . . . . . . . . . . 18
|
16 | | opabid 4982 |
. . . . . . . . . . . . . . . . . 18
|
17 | 14, 15, 16 | 3bitri 286 |
. . . . . . . . . . . . . . . . 17
|
18 | 12, 17 | syl6bbr 278 |
. . . . . . . . . . . . . . . 16
|
19 | 11, 18 | sylan2 491 |
. . . . . . . . . . . . . . 15
|
20 | 19 | rexbidva 3049 |
. . . . . . . . . . . . . 14
|
21 | 20 | ralbiia 2979 |
. . . . . . . . . . . . 13
|
22 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
|
23 | 22 | rexbidv 3052 |
. . . . . . . . . . . . . . 15
|
24 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
25 | | nfrab1 3122 |
. . . . . . . . . . . . . . . 16
|
26 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
27 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . 17
|
28 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
29 | 26, 27, 28 | nfbr 4699 |
. . . . . . . . . . . . . . . 16
|
30 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
|
31 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
|
32 | 24, 25, 29, 30, 31 | cbvrexf 3166 |
. . . . . . . . . . . . . . 15
|
33 | 23, 32 | syl6bb 276 |
. . . . . . . . . . . . . 14
|
34 | 33 | cbvralv 3171 |
. . . . . . . . . . . . 13
|
35 | 21, 34 | bitr4i 267 |
. . . . . . . . . . . 12
|
36 | 10, 35 | sylib 208 |
. . . . . . . . . . 11
|
37 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
38 | 25 | nfcri 2758 |
. . . . . . . . . . . . . . 15
|
39 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | nfeq2 2780 |
. . . . . . . . . . . . . . 15
|
41 | 38, 40 | nfan 1828 |
. . . . . . . . . . . . . 14
|
42 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
43 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
45 | 42, 44 | anbi12d 747 |
. . . . . . . . . . . . . 14
|
46 | 37, 41, 45 | cbvopab1 4723 |
. . . . . . . . . . . . 13
|
47 | | df-mpt 4730 |
. . . . . . . . . . . . 13
|
48 | 46, 13, 47 | 3eqtr4i 2654 |
. . . . . . . . . . . 12
|
49 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
50 | 39 | nfel1 2779 |
. . . . . . . . . . . . . 14
|
51 | 43 | eleq1d 2686 |
. . . . . . . . . . . . . 14
|
52 | 26, 49, 50, 51 | elrabf 3360 |
. . . . . . . . . . . . 13
|
53 | 52 | simprbi 480 |
. . . . . . . . . . . 12
|
54 | 48, 53 | fmpti 6383 |
. . . . . . . . . . 11
|
55 | 36, 54 | jctil 560 |
. . . . . . . . . 10
|
56 | | dffo4 6375 |
. . . . . . . . . 10
|
57 | 55, 56 | sylibr 224 |
. . . . . . . . 9
|
58 | 57 | adantl 482 |
. . . . . . . 8
|
59 | | relen 7960 |
. . . . . . . . . . . . 13
|
60 | 59 | brrelex2i 5159 |
. . . . . . . . . . . 12
|
61 | | ssrab2 3687 |
. . . . . . . . . . . 12
|
62 | | ssdomg 8001 |
. . . . . . . . . . . 12
|
63 | 60, 61, 62 | mpisyl 21 |
. . . . . . . . . . 11
|
64 | | ensym 8005 |
. . . . . . . . . . 11
|
65 | | domentr 8015 |
. . . . . . . . . . 11
|
66 | 63, 64, 65 | syl2anc 693 |
. . . . . . . . . 10
|
67 | 66 | ad2antlr 763 |
. . . . . . . . 9
|
68 | | enfi 8176 |
. . . . . . . . . . . 12
|
69 | 68 | biimpac 503 |
. . . . . . . . . . 11
|
70 | | rabfi 8185 |
. . . . . . . . . . 11
|
71 | 69, 70 | syl 17 |
. . . . . . . . . 10
|
72 | | fodomfi 8239 |
. . . . . . . . . 10
|
73 | 71, 57, 72 | syl2an 494 |
. . . . . . . . 9
|
74 | | sbth 8080 |
. . . . . . . . 9
|
75 | 67, 73, 74 | syl2anc 693 |
. . . . . . . 8
|
76 | | simpll 790 |
. . . . . . . 8
|
77 | | fofinf1o 8241 |
. . . . . . . 8
|
78 | 58, 75, 76, 77 | syl3anc 1326 |
. . . . . . 7
|
79 | | f1of1 6136 |
. . . . . . 7
|
80 | 78, 79 | syl 17 |
. . . . . 6
|
81 | | dff12 6100 |
. . . . . . . 8
|
82 | 81 | simprbi 480 |
. . . . . . 7
|
83 | 22 | mobidv 2491 |
. . . . . . . . 9
|
84 | 29, 30, 31 | cbvmo 2506 |
. . . . . . . . 9
|
85 | 83, 84 | syl6bb 276 |
. . . . . . . 8
|
86 | 85 | cbvalv 2273 |
. . . . . . 7
|
87 | 82, 86 | sylib 208 |
. . . . . 6
|
88 | | mormo 3158 |
. . . . . . 7
|
89 | 88 | alimi 1739 |
. . . . . 6
|
90 | | alral 2928 |
. . . . . 6
|
91 | 80, 87, 89, 90 | 4syl 19 |
. . . . 5
|
92 | 18 | rmobidva 3130 |
. . . . . 6
|
93 | 92 | ralbiia 2979 |
. . . . 5
|
94 | 91, 93 | sylibr 224 |
. . . 4
|
95 | 94 | ex 450 |
. . 3
|
96 | 95 | pm4.71d 666 |
. 2
|
97 | | reu5 3159 |
. . . 4
|
98 | 97 | ralbii 2980 |
. . 3
|
99 | | r19.26 3064 |
. . 3
|
100 | 98, 99 | bitri 264 |
. 2
|
101 | 96, 100 | syl6bbr 278 |
1
|