Step | Hyp | Ref
| Expression |
1 | | raleq 3138 |
. . . 4
|
2 | | feq2 6027 |
. . . . . 6
|
3 | | raleq 3138 |
. . . . . 6
|
4 | 2, 3 | anbi12d 747 |
. . . . 5
|
5 | 4 | exbidv 1850 |
. . . 4
|
6 | 1, 5 | imbi12d 334 |
. . 3
|
7 | | raleq 3138 |
. . . 4
|
8 | | feq2 6027 |
. . . . . 6
|
9 | | raleq 3138 |
. . . . . 6
|
10 | 8, 9 | anbi12d 747 |
. . . . 5
|
11 | 10 | exbidv 1850 |
. . . 4
|
12 | 7, 11 | imbi12d 334 |
. . 3
|
13 | | raleq 3138 |
. . . 4
|
14 | | feq2 6027 |
. . . . . . 7
|
15 | | raleq 3138 |
. . . . . . 7
|
16 | 14, 15 | anbi12d 747 |
. . . . . 6
|
17 | 16 | exbidv 1850 |
. . . . 5
|
18 | | feq1 6026 |
. . . . . . 7
|
19 | | fvex 6201 |
. . . . . . . . . 10
|
20 | | ac6sfi.1 |
. . . . . . . . . 10
|
21 | 19, 20 | sbcie 3470 |
. . . . . . . . 9
|
22 | | fveq1 6190 |
. . . . . . . . . 10
|
23 | 22 | sbceq1d 3440 |
. . . . . . . . 9
|
24 | 21, 23 | syl5bbr 274 |
. . . . . . . 8
|
25 | 24 | ralbidv 2986 |
. . . . . . 7
|
26 | 18, 25 | anbi12d 747 |
. . . . . 6
|
27 | 26 | cbvexv 2275 |
. . . . 5
|
28 | 17, 27 | syl6bb 276 |
. . . 4
|
29 | 13, 28 | imbi12d 334 |
. . 3
|
30 | | raleq 3138 |
. . . 4
|
31 | | feq2 6027 |
. . . . . 6
|
32 | | raleq 3138 |
. . . . . 6
|
33 | 31, 32 | anbi12d 747 |
. . . . 5
|
34 | 33 | exbidv 1850 |
. . . 4
|
35 | 30, 34 | imbi12d 334 |
. . 3
|
36 | | f0 6086 |
. . . 4
|
37 | | 0ex 4790 |
. . . . 5
|
38 | | ral0 4076 |
. . . . . . 7
|
39 | 38 | biantru 526 |
. . . . . 6
|
40 | | feq1 6026 |
. . . . . 6
|
41 | 39, 40 | syl5bbr 274 |
. . . . 5
|
42 | 37, 41 | spcev 3300 |
. . . 4
|
43 | 36, 42 | mp1i 13 |
. . 3
|
44 | | ssun1 3776 |
. . . . . . 7
|
45 | | ssralv 3666 |
. . . . . . 7
|
46 | 44, 45 | ax-mp 5 |
. . . . . 6
|
47 | 46 | imim1i 63 |
. . . . 5
|
48 | | ssun2 3777 |
. . . . . . . . 9
|
49 | | ssralv 3666 |
. . . . . . . . 9
|
50 | 48, 49 | ax-mp 5 |
. . . . . . . 8
|
51 | | vex 3203 |
. . . . . . . . . 10
|
52 | | ralsnsg 4216 |
. . . . . . . . . 10
|
53 | 51, 52 | ax-mp 5 |
. . . . . . . . 9
|
54 | | sbcrex 3514 |
. . . . . . . . 9
|
55 | 53, 54 | bitri 264 |
. . . . . . . 8
|
56 | 50, 55 | sylib 208 |
. . . . . . 7
|
57 | | nfv 1843 |
. . . . . . . 8
|
58 | | nfv 1843 |
. . . . . . . . 9
|
59 | | nfv 1843 |
. . . . . . . . . . 11
|
60 | | nfcv 2764 |
. . . . . . . . . . . 12
|
61 | | nfsbc1v 3455 |
. . . . . . . . . . . 12
|
62 | 60, 61 | nfral 2945 |
. . . . . . . . . . 11
|
63 | 59, 62 | nfan 1828 |
. . . . . . . . . 10
|
64 | 63 | nfex 2154 |
. . . . . . . . 9
|
65 | 58, 64 | nfim 1825 |
. . . . . . . 8
|
66 | | simprl 794 |
. . . . . . . . . . . . 13
|
67 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
68 | 51, 67 | f1osn 6176 |
. . . . . . . . . . . . . . 15
|
69 | | f1of 6137 |
. . . . . . . . . . . . . . 15
|
70 | 68, 69 | mp1i 13 |
. . . . . . . . . . . . . 14
|
71 | | simpl2 1065 |
. . . . . . . . . . . . . . 15
|
72 | 71 | snssd 4340 |
. . . . . . . . . . . . . 14
|
73 | 70, 72 | fssd 6057 |
. . . . . . . . . . . . 13
|
74 | | simpl1 1064 |
. . . . . . . . . . . . . 14
|
75 | | disjsn 4246 |
. . . . . . . . . . . . . 14
|
76 | 74, 75 | sylibr 224 |
. . . . . . . . . . . . 13
|
77 | | fun2 6067 |
. . . . . . . . . . . . 13
|
78 | 66, 73, 76, 77 | syl21anc 1325 |
. . . . . . . . . . . 12
|
79 | | simprr 796 |
. . . . . . . . . . . . . 14
|
80 | | eleq1a 2696 |
. . . . . . . . . . . . . . . . . . 19
|
81 | 80 | necon3bd 2808 |
. . . . . . . . . . . . . . . . . 18
|
82 | 81 | impcom 446 |
. . . . . . . . . . . . . . . . 17
|
83 | | fvunsn 6445 |
. . . . . . . . . . . . . . . . 17
|
84 | | dfsbcq 3437 |
. . . . . . . . . . . . . . . . . 18
|
85 | 84, 21 | syl6rbb 277 |
. . . . . . . . . . . . . . . . 17
|
86 | 82, 83, 85 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
87 | 86 | ralbidva 2985 |
. . . . . . . . . . . . . . 15
|
88 | 74, 87 | syl 17 |
. . . . . . . . . . . . . 14
|
89 | 79, 88 | mpbid 222 |
. . . . . . . . . . . . 13
|
90 | | simpl3 1066 |
. . . . . . . . . . . . . 14
|
91 | | ffun 6048 |
. . . . . . . . . . . . . . . . 17
|
92 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . 18
|
93 | | vsnid 4209 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 67 | dmsnop 5609 |
. . . . . . . . . . . . . . . . . . 19
|
95 | 93, 94 | eleqtrri 2700 |
. . . . . . . . . . . . . . . . . 18
|
96 | | funssfv 6209 |
. . . . . . . . . . . . . . . . . 18
|
97 | 92, 95, 96 | mp3an23 1416 |
. . . . . . . . . . . . . . . . 17
|
98 | 78, 91, 97 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
99 | 51, 67 | fvsn 6446 |
. . . . . . . . . . . . . . . 16
|
100 | 98, 99 | syl6req 2673 |
. . . . . . . . . . . . . . 15
|
101 | | ralsnsg 4216 |
. . . . . . . . . . . . . . . . 17
|
102 | 51, 101 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
103 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . 21
|
104 | 103 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
105 | 104 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . 19
|
106 | 105 | biimparc 504 |
. . . . . . . . . . . . . . . . . 18
|
107 | | sbceq1a 3446 |
. . . . . . . . . . . . . . . . . 18
|
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
109 | 108 | ralbidva 2985 |
. . . . . . . . . . . . . . . 16
|
110 | 102, 109 | syl5bbr 274 |
. . . . . . . . . . . . . . 15
|
111 | 100, 110 | syl 17 |
. . . . . . . . . . . . . 14
|
112 | 90, 111 | mpbid 222 |
. . . . . . . . . . . . 13
|
113 | | ralun 3795 |
. . . . . . . . . . . . 13
|
114 | 89, 112, 113 | syl2anc 693 |
. . . . . . . . . . . 12
|
115 | | vex 3203 |
. . . . . . . . . . . . . 14
|
116 | | snex 4908 |
. . . . . . . . . . . . . 14
|
117 | 115, 116 | unex 6956 |
. . . . . . . . . . . . 13
|
118 | | feq1 6026 |
. . . . . . . . . . . . . 14
|
119 | | fveq1 6190 |
. . . . . . . . . . . . . . . 16
|
120 | 119 | sbceq1d 3440 |
. . . . . . . . . . . . . . 15
|
121 | 120 | ralbidv 2986 |
. . . . . . . . . . . . . 14
|
122 | 118, 121 | anbi12d 747 |
. . . . . . . . . . . . 13
|
123 | 117, 122 | spcev 3300 |
. . . . . . . . . . . 12
|
124 | 78, 114, 123 | syl2anc 693 |
. . . . . . . . . . 11
|
125 | 124 | ex 450 |
. . . . . . . . . 10
|
126 | 125 | exlimdv 1861 |
. . . . . . . . 9
|
127 | 126 | 3exp 1264 |
. . . . . . . 8
|
128 | 57, 65, 127 | rexlimd 3026 |
. . . . . . 7
|
129 | 56, 128 | syl5 34 |
. . . . . 6
|
130 | 129 | a2d 29 |
. . . . 5
|
131 | 47, 130 | syl5 34 |
. . . 4
|
132 | 131 | adantl 482 |
. . 3
|
133 | 6, 12, 29, 35, 43, 132 | findcard2s 8201 |
. 2
|
134 | 133 | imp 445 |
1
|