Step | Hyp | Ref
| Expression |
1 | | enfii 6768 |
. . . 4
|
2 | 1 | 3adant2 1000 |
. . 3
|
3 | | sseq1 3120 |
. . . . . . 7
|
4 | | breq1 3932 |
. . . . . . 7
|
5 | 3, 4 | anbi12d 464 |
. . . . . 6
|
6 | | eqeq1 2146 |
. . . . . 6
|
7 | 5, 6 | imbi12d 233 |
. . . . 5
|
8 | 7 | albidv 1796 |
. . . 4
|
9 | | sseq1 3120 |
. . . . . . 7
|
10 | | breq1 3932 |
. . . . . . 7
|
11 | 9, 10 | anbi12d 464 |
. . . . . 6
|
12 | | eqeq1 2146 |
. . . . . 6
|
13 | 11, 12 | imbi12d 233 |
. . . . 5
|
14 | 13 | albidv 1796 |
. . . 4
|
15 | | sseq1 3120 |
. . . . . . 7
|
16 | | breq1 3932 |
. . . . . . 7
|
17 | 15, 16 | anbi12d 464 |
. . . . . 6
|
18 | | eqeq1 2146 |
. . . . . 6
|
19 | 17, 18 | imbi12d 233 |
. . . . 5
|
20 | 19 | albidv 1796 |
. . . 4
|
21 | | sseq1 3120 |
. . . . . . 7
|
22 | | breq1 3932 |
. . . . . . 7
|
23 | 21, 22 | anbi12d 464 |
. . . . . 6
|
24 | | eqeq1 2146 |
. . . . . 6
|
25 | 23, 24 | imbi12d 233 |
. . . . 5
|
26 | 25 | albidv 1796 |
. . . 4
|
27 | | ensym 6675 |
. . . . . . . 8
|
28 | | en0 6689 |
. . . . . . . 8
|
29 | 27, 28 | sylib 121 |
. . . . . . 7
|
30 | 29 | eqcomd 2145 |
. . . . . 6
|
31 | 30 | adantl 275 |
. . . . 5
|
32 | 31 | ax-gen 1425 |
. . . 4
|
33 | | sseq2 3121 |
. . . . . . . 8
|
34 | | breq2 3933 |
. . . . . . . 8
|
35 | 33, 34 | anbi12d 464 |
. . . . . . 7
|
36 | | eqeq2 2149 |
. . . . . . 7
|
37 | 35, 36 | imbi12d 233 |
. . . . . 6
|
38 | 37 | cbvalv 1889 |
. . . . 5
|
39 | | simplr 519 |
. . . . . . . . . . 11
|
40 | | difun2 3442 |
. . . . . . . . . . . . . 14
|
41 | | difsn 3657 |
. . . . . . . . . . . . . . 15
|
42 | 41 | ad3antlr 484 |
. . . . . . . . . . . . . 14
|
43 | 40, 42 | syl5eq 2184 |
. . . . . . . . . . . . 13
|
44 | | simprl 520 |
. . . . . . . . . . . . . 14
|
45 | 44 | ssdifd 3212 |
. . . . . . . . . . . . 13
|
46 | 43, 45 | eqsstrrd 3134 |
. . . . . . . . . . . 12
|
47 | | simplll 522 |
. . . . . . . . . . . . . . 15
|
48 | | vex 2689 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | a1i 9 |
. . . . . . . . . . . . . . 15
|
50 | | simpllr 523 |
. . . . . . . . . . . . . . 15
|
51 | | unsnfi 6807 |
. . . . . . . . . . . . . . 15
|
52 | 47, 49, 50, 51 | syl3anc 1216 |
. . . . . . . . . . . . . 14
|
53 | | simprr 521 |
. . . . . . . . . . . . . 14
|
54 | | vsnid 3557 |
. . . . . . . . . . . . . . . 16
|
55 | | elun2 3244 |
. . . . . . . . . . . . . . . 16
|
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
57 | 56 | a1i 9 |
. . . . . . . . . . . . . 14
|
58 | 44, 57 | sseldd 3098 |
. . . . . . . . . . . . . 14
|
59 | 52, 53, 57, 58 | dif1enen 6774 |
. . . . . . . . . . . . 13
|
60 | 43, 59 | eqbrtrrd 3952 |
. . . . . . . . . . . 12
|
61 | 46, 60 | jca 304 |
. . . . . . . . . . 11
|
62 | | vex 2689 |
. . . . . . . . . . . . 13
|
63 | | difexg 4069 |
. . . . . . . . . . . . 13
|
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . 12
|
65 | | sseq2 3121 |
. . . . . . . . . . . . . 14
|
66 | | breq2 3933 |
. . . . . . . . . . . . . 14
|
67 | 65, 66 | anbi12d 464 |
. . . . . . . . . . . . 13
|
68 | | eqeq2 2149 |
. . . . . . . . . . . . 13
|
69 | 67, 68 | imbi12d 233 |
. . . . . . . . . . . 12
|
70 | 64, 69 | spcv 2779 |
. . . . . . . . . . 11
|
71 | 39, 61, 70 | sylc 62 |
. . . . . . . . . 10
|
72 | 71 | uneq1d 3229 |
. . . . . . . . 9
|
73 | 53 | ensymd 6677 |
. . . . . . . . . . 11
|
74 | | enfii 6768 |
. . . . . . . . . . 11
|
75 | 52, 73, 74 | syl2anc 408 |
. . . . . . . . . 10
|
76 | | fidifsnid 6765 |
. . . . . . . . . 10
|
77 | 75, 58, 76 | syl2anc 408 |
. . . . . . . . 9
|
78 | 72, 77 | eqtrd 2172 |
. . . . . . . 8
|
79 | 78 | ex 114 |
. . . . . . 7
|
80 | 79 | alrimiv 1846 |
. . . . . 6
|
81 | 80 | ex 114 |
. . . . 5
|
82 | 38, 81 | syl5bi 151 |
. . . 4
|
83 | 8, 14, 20, 26, 32, 82 | findcard2s 6784 |
. . 3
|
84 | 2, 83 | syl 14 |
. 2
|
85 | | 3simpc 980 |
. 2
|
86 | | sseq2 3121 |
. . . . . 6
|
87 | | breq2 3933 |
. . . . . 6
|
88 | 86, 87 | anbi12d 464 |
. . . . 5
|
89 | | eqeq2 2149 |
. . . . 5
|
90 | 88, 89 | imbi12d 233 |
. . . 4
|
91 | 90 | spcgv 2773 |
. . 3
|
92 | 91 | 3ad2ant1 1002 |
. 2
|
93 | 84, 85, 92 | mp2d 47 |
1
|