Step | Hyp | Ref
| Expression |
1 | | fbasrn.c |
. . 3
|
2 | | simpl2 1065 |
. . . . . . 7
|
3 | | imassrn 5477 |
. . . . . . . 8
|
4 | | frn 6053 |
. . . . . . . 8
|
5 | 3, 4 | syl5ss 3614 |
. . . . . . 7
|
6 | 2, 5 | syl 17 |
. . . . . 6
|
7 | | simpl3 1066 |
. . . . . . 7
|
8 | | elpw2g 4827 |
. . . . . . 7
|
9 | 7, 8 | syl 17 |
. . . . . 6
|
10 | 6, 9 | mpbird 247 |
. . . . 5
|
11 | | eqid 2622 |
. . . . 5
|
12 | 10, 11 | fmptd 6385 |
. . . 4
|
13 | | frn 6053 |
. . . 4
|
14 | 12, 13 | syl 17 |
. . 3
|
15 | 1, 14 | syl5eqss 3649 |
. 2
|
16 | 1 | a1i 11 |
. . . 4
|
17 | | ffun 6048 |
. . . . . . . 8
|
18 | 17 | 3ad2ant2 1083 |
. . . . . . 7
|
19 | | funimaexg 5975 |
. . . . . . . 8
|
20 | 19 | ralrimiva 2966 |
. . . . . . 7
|
21 | | dmmptg 5632 |
. . . . . . 7
|
22 | 18, 20, 21 | 3syl 18 |
. . . . . 6
|
23 | | fbasne0 21634 |
. . . . . . 7
|
24 | 23 | 3ad2ant1 1082 |
. . . . . 6
|
25 | 22, 24 | eqnetrd 2861 |
. . . . 5
|
26 | | dm0rn0 5342 |
. . . . . 6
|
27 | 26 | necon3bii 2846 |
. . . . 5
|
28 | 25, 27 | sylib 208 |
. . . 4
|
29 | 16, 28 | eqnetrd 2861 |
. . 3
|
30 | | fbelss 21637 |
. . . . . . . . 9
|
31 | 30 | ex 450 |
. . . . . . . 8
|
32 | 31 | 3ad2ant1 1082 |
. . . . . . 7
|
33 | | 0nelfb 21635 |
. . . . . . . . . 10
|
34 | | eleq1 2689 |
. . . . . . . . . . 11
|
35 | 34 | notbid 308 |
. . . . . . . . . 10
|
36 | 33, 35 | syl5ibrcom 237 |
. . . . . . . . 9
|
37 | 36 | con2d 129 |
. . . . . . . 8
|
38 | 37 | 3ad2ant1 1082 |
. . . . . . 7
|
39 | 32, 38 | jcad 555 |
. . . . . 6
|
40 | | fdm 6051 |
. . . . . . . . . . . . . . 15
|
41 | 40 | 3ad2ant2 1083 |
. . . . . . . . . . . . . 14
|
42 | 41 | sseq2d 3633 |
. . . . . . . . . . . . 13
|
43 | 42 | biimpar 502 |
. . . . . . . . . . . 12
|
44 | | sseqin2 3817 |
. . . . . . . . . . . 12
|
45 | 43, 44 | sylib 208 |
. . . . . . . . . . 11
|
46 | 45 | eqeq1d 2624 |
. . . . . . . . . 10
|
47 | 46 | biimpd 219 |
. . . . . . . . 9
|
48 | 47 | con3d 148 |
. . . . . . . 8
|
49 | 48 | expimpd 629 |
. . . . . . 7
|
50 | | eqcom 2629 |
. . . . . . . . 9
|
51 | | imadisj 5484 |
. . . . . . . . 9
|
52 | 50, 51 | bitri 264 |
. . . . . . . 8
|
53 | 52 | notbii 310 |
. . . . . . 7
|
54 | 49, 53 | syl6ibr 242 |
. . . . . 6
|
55 | 39, 54 | syld 47 |
. . . . 5
|
56 | 55 | ralrimiv 2965 |
. . . 4
|
57 | 1 | eleq2i 2693 |
. . . . . . 7
|
58 | | 0ex 4790 |
. . . . . . . 8
|
59 | 11 | elrnmpt 5372 |
. . . . . . . 8
|
60 | 58, 59 | ax-mp 5 |
. . . . . . 7
|
61 | 57, 60 | bitri 264 |
. . . . . 6
|
62 | 61 | notbii 310 |
. . . . 5
|
63 | | df-nel 2898 |
. . . . 5
|
64 | | ralnex 2992 |
. . . . 5
|
65 | 62, 63, 64 | 3bitr4i 292 |
. . . 4
|
66 | 56, 65 | sylibr 224 |
. . 3
|
67 | 1 | eleq2i 2693 |
. . . . . . . 8
|
68 | | vex 3203 |
. . . . . . . . 9
|
69 | | imaeq2 5462 |
. . . . . . . . . . 11
|
70 | 69 | cbvmptv 4750 |
. . . . . . . . . 10
|
71 | 70 | elrnmpt 5372 |
. . . . . . . . 9
|
72 | 68, 71 | ax-mp 5 |
. . . . . . . 8
|
73 | 67, 72 | bitri 264 |
. . . . . . 7
|
74 | 1 | eleq2i 2693 |
. . . . . . . 8
|
75 | | vex 3203 |
. . . . . . . . 9
|
76 | | imaeq2 5462 |
. . . . . . . . . . 11
|
77 | 76 | cbvmptv 4750 |
. . . . . . . . . 10
|
78 | 77 | elrnmpt 5372 |
. . . . . . . . 9
|
79 | 75, 78 | ax-mp 5 |
. . . . . . . 8
|
80 | 74, 79 | bitri 264 |
. . . . . . 7
|
81 | 73, 80 | anbi12i 733 |
. . . . . 6
|
82 | | reeanv 3107 |
. . . . . 6
|
83 | 81, 82 | bitr4i 267 |
. . . . 5
|
84 | | fbasssin 21640 |
. . . . . . . . . . 11
|
85 | 84 | 3expb 1266 |
. . . . . . . . . 10
|
86 | 85 | 3ad2antl1 1223 |
. . . . . . . . 9
|
87 | 86 | adantrr 753 |
. . . . . . . 8
|
88 | | eqid 2622 |
. . . . . . . . . . . . 13
|
89 | | imaeq2 5462 |
. . . . . . . . . . . . . . 15
|
90 | 89 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
91 | 90 | rspcev 3309 |
. . . . . . . . . . . . 13
|
92 | 88, 91 | mpan2 707 |
. . . . . . . . . . . 12
|
93 | 92 | ad2antrl 764 |
. . . . . . . . . . 11
|
94 | 1 | eleq2i 2693 |
. . . . . . . . . . . . 13
|
95 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
96 | 95 | funimaex 5976 |
. . . . . . . . . . . . . 14
|
97 | 11 | elrnmpt 5372 |
. . . . . . . . . . . . . 14
|
98 | 18, 96, 97 | 3syl 18 |
. . . . . . . . . . . . 13
|
99 | 94, 98 | syl5bb 272 |
. . . . . . . . . . . 12
|
100 | 99 | ad2antrr 762 |
. . . . . . . . . . 11
|
101 | 93, 100 | mpbird 247 |
. . . . . . . . . 10
|
102 | | imass2 5501 |
. . . . . . . . . . . 12
|
103 | 102 | ad2antll 765 |
. . . . . . . . . . 11
|
104 | | inss1 3833 |
. . . . . . . . . . . . . 14
|
105 | | imass2 5501 |
. . . . . . . . . . . . . 14
|
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . . . . 13
|
107 | | inss2 3834 |
. . . . . . . . . . . . . 14
|
108 | | imass2 5501 |
. . . . . . . . . . . . . 14
|
109 | 107, 108 | ax-mp 5 |
. . . . . . . . . . . . 13
|
110 | 106, 109 | ssini 3836 |
. . . . . . . . . . . 12
|
111 | | ineq12 3809 |
. . . . . . . . . . . . 13
|
112 | 111 | ad2antlr 763 |
. . . . . . . . . . . 12
|
113 | 110, 112 | syl5sseqr 3654 |
. . . . . . . . . . 11
|
114 | 103, 113 | sstrd 3613 |
. . . . . . . . . 10
|
115 | | sseq1 3626 |
. . . . . . . . . . 11
|
116 | 115 | rspcev 3309 |
. . . . . . . . . 10
|
117 | 101, 114,
116 | syl2anc 693 |
. . . . . . . . 9
|
118 | 117 | adantlrl 756 |
. . . . . . . 8
|
119 | 87, 118 | rexlimddv 3035 |
. . . . . . 7
|
120 | 119 | exp32 631 |
. . . . . 6
|
121 | 120 | rexlimdvv 3037 |
. . . . 5
|
122 | 83, 121 | syl5bi 232 |
. . . 4
|
123 | 122 | ralrimivv 2970 |
. . 3
|
124 | 29, 66, 123 | 3jca 1242 |
. 2
|
125 | | isfbas2 21639 |
. . 3
|
126 | 125 | 3ad2ant3 1084 |
. 2
|
127 | 15, 124, 126 | mpbir2and 957 |
1
|