Step Hyp Ref
Expression 1 rabn0 3805 . . . . . 6
2 rexnal 2905 . . . . . 6
3 1 , 2 bitri 249 . . . . 5
4 simpl1 999 . . . . . . . . 9
5 simpl2 1000 . . . . . . . . 9
6 ssrab2 3584 . . . . . . . . . 10
7 6 a1i 11 . . . . . . . . 9
8 simpr 461 . . . . . . . . 9
9 wereu2 4881 . . . . . . . . 9
10 4 , 5 , 7 , 8 , 9 syl22anc 1229 . . . . . . . 8
11 reurex 3074 . . . . . . . 8
12 10 , 11 syl 16 . . . . . . 7
13 12 ex 434 . . . . . 6
14 fveq2 5871 . . . . . . . . . . 11
15 id 22 . . . . . . . . . . 11
16 14 , 15 eqeq12d 2479 . . . . . . . . . 10
17 16 notbid 294 . . . . . . . . 9
18 17 elrab 3257 . . . . . . . 8
19 fveq2 5871 . . . . . . . . . . . . . 14
20 id 22 . . . . . . . . . . . . . 14
21 19 , 20 eqeq12d 2479 . . . . . . . . . . . . 13
22 21 notbid 294 . . . . . . . . . . . 12
23 22 ralrab 3261 . . . . . . . . . . 11
24 con34b 292 . . . . . . . . . . . . 13
25 24 bicomi 202 . . . . . . . . . . . 12
26 25 ralbii 2888 . . . . . . . . . . 11
27 23 , 26 bitri 249 . . . . . . . . . 10
28 simpl3 1001 . . . . . . . . . . . . . . . . . 18
29 isof1o 6221 . . . . . . . . . . . . . . . . . 18
30 28 , 29 syl 16 . . . . . . . . . . . . . . . . 17
31 f1of 5821 . . . . . . . . . . . . . . . . 17
32 30 , 31 syl 16 . . . . . . . . . . . . . . . 16
33 simprl 756 . . . . . . . . . . . . . . . 16
34 32 , 33 ffvelrnd 6032 . . . . . . . . . . . . . . 15
35 breq1 4455 . . . . . . . . . . . . . . . . 17
36 fveq2 5871 . . . . . . . . . . . . . . . . . 18
37 id 22 . . . . . . . . . . . . . . . . . 18
38 36 , 37 eqeq12d 2479 . . . . . . . . . . . . . . . . 17
39 35 , 38 imbi12d 320 . . . . . . . . . . . . . . . 16
40 39 rspcv 3206 . . . . . . . . . . . . . . 15
41 34 , 40 syl 16 . . . . . . . . . . . . . 14
42 41 com23 78 . . . . . . . . . . . . 13
43 42 imp 429 . . . . . . . . . . . 12
44 f1of1 5820 . . . . . . . . . . . . . . . 16
45 30 , 44 syl 16 . . . . . . . . . . . . . . 15
46 f1fveq 6170 . . . . . . . . . . . . . . 15
47 45 , 34 , 33 , 46 syl12anc 1226 . . . . . . . . . . . . . 14
48 pm2.21 108 . . . . . . . . . . . . . . 15
49 48 ad2antll 728 . . . . . . . . . . . . . 14
50 47 , 49 sylbid 215 . . . . . . . . . . . . 13
51 50 adantr 465 . . . . . . . . . . . 12
52 43 , 51 syld 44 . . . . . . . . . . 11
53 f1ocnv 5833 . . . . . . . . . . . . . . . 16
54 f1of 5821 . . . . . . . . . . . . . . . 16
55 30 , 53 , 54 3syl 20 . . . . . . . . . . . . . . 15
56 55 , 33 ffvelrnd 6032 . . . . . . . . . . . . . 14
57 56 adantr 465 . . . . . . . . . . . . 13
58 isorel 6222 . . . . . . . . . . . . . . . 16
59 28 , 56 , 33 , 58 syl12anc 1226 . . . . . . . . . . . . . . 15
60 f1ocnvfv2 6183 . . . . . . . . . . . . . . . . 17
61 30 , 33 , 60 syl2anc 661 . . . . . . . . . . . . . . . 16
62 61 breq1d 4462 . . . . . . . . . . . . . . 15
63 59 , 62 bitr2d 254 . . . . . . . . . . . . . 14
64 63 biimpa 484 . . . . . . . . . . . . 13
65 breq1 4455 . . . . . . . . . . . . . . . 16
66 fveq2 5871 . . . . . . . . . . . . . . . . 17
67 id 22 . . . . . . . . . . . . . . . . 17
68 66 , 67 eqeq12d 2479 . . . . . . . . . . . . . . . 16
69 65 , 68 imbi12d 320 . . . . . . . . . . . . . . 15
70 69 rspcv 3206 . . . . . . . . . . . . . 14
71 70 com23 78 . . . . . . . . . . . . 13
72 57 , 64 , 71 sylc 60 . . . . . . . . . . . 12
73 simplrr 762 . . . . . . . . . . . . . . 15
74 fveq2 5871 . . . . . . . . . . . . . . . . 17
75 74 adantl 466 . . . . . . . . . . . . . . . 16
76 61 fveq2d 5875 . . . . . . . . . . . . . . . . 17
77 76 adantr 465 . . . . . . . . . . . . . . . 16
78 61 adantr 465 . . . . . . . . . . . . . . . 16
79 75 , 77 , 78 3eqtr3d 2506 . . . . . . . . . . . . . . 15
80 73 , 79 , 48 sylc 60 . . . . . . . . . . . . . 14
81 80 ex 434 . . . . . . . . . . . . 13
82 81 adantr 465 . . . . . . . . . . . 12
83 72 , 82 syld 44 . . . . . . . . . . 11
84 simprr 757 . . . . . . . . . . . 12
85 simpl1 999 . . . . . . . . . . . . . . 15
86 weso 4875 . . . . . . . . . . . . . . 15
87 85 , 86 syl 16 . . . . . . . . . . . . . 14
88 sotrieq 4832 . . . . . . . . . . . . . 14
89 87 , 34 , 33 , 88 syl12anc 1226 . . . . . . . . . . . . 13
90 89 con2bid 329 . . . . . . . . . . . 12
91 84 , 90 mpbird 232 . . . . . . . . . . 11
92 52 , 83 , 91 mpjaodan 786 . . . . . . . . . 10
93 27 , 92 syl5bi 217 . . . . . . . . 9
94 93 ex 434 . . . . . . . 8
95 18 , 94 syl5bi 217 . . . . . . 7
96 95 rexlimdv 2947 . . . . . 6
97 13 , 96 syld 44 . . . . 5
98 3 , 97 syl5bir 218 . . . 4
99 98 pm2.18d 111 . . 3
100 fvresi 6097 . . . . . 6
101 100 eqeq2d 2471 . . . . 5
102 101 biimprd 223 . . . 4
103 102 ralimia 2848 . . 3
104 99 , 103 syl 16 . 2
105 29 3ad2ant3 1019 . . . 4
106 f1ofn 5822 . . . 4
107 105 , 106 syl 16 . . 3
108 fnresi 5703 . . . 4
109 108 a1i 11 . . 3
110 eqfnfv 5981 . . 3
111 107 , 109 ,
110 syl2anc 661 . 2
112 104 , 111 mpbird 232 1
