Step Hyp Ref
Expression 1 f1f 5786 . . 3
2 fo2ndf 6907 . . 3
3 1 , 2 syl 16 . 2
4 f2ndf 6906 . . . . 5
5 1 , 4 syl 16 . . . 4
6 fssxp 5748 . . . . . . 7
7 1 , 6 syl 16 . . . . . 6
8 ssel2 3498 . . . . . . . . . . 11
9 elxp2 5022 . . . . . . . . . . 11
10 8 , 9 sylib 196 . . . . . . . . . 10
11 ssel2 3498 . . . . . . . . . . 11
12 elxp2 5022 . . . . . . . . . . 11
13 11 , 12 sylib 196 . . . . . . . . . 10
14 10 , 13 anim12dan 837 . . . . . . . . 9
15 fvres 5885 . . . . . . . . . . . . . . . . . . . . . . . . 25
16 15 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
17 16 adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
18 fvres 5885 . . . . . . . . . . . . . . . . . . . . . . . 24
19 18 ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . 23
20 17 , 19 eqeq12d 2479 . . . . . . . . . . . . . . . . . . . . . 22
21 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . 25
22 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . 25
23 21 , 22 op2nd 6809 . . . . . . . . . . . . . . . . . . . . . . . 24
24 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . 25
25 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . 25
26 24 , 25 op2nd 6809 . . . . . . . . . . . . . . . . . . . . . . . 24
27 23 , 26 eqeq12i 2477 . . . . . . . . . . . . . . . . . . . . . . 23
28 f1fun 5788 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
29 funopfv 5912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
30 funopfv 5912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
31 29 , 30 anim12d 563 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
32 28 , 31 syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
33 eqcom 2466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
34 33 biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
35 eqcom 2466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
36 35 biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
37 34 , 36 eqeqan12d 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
38 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
39 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
40 38 , 39 anim12i 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
41 f1veqaeq 6168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
42 40 , 41 sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
43 opeq12 4219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
44 43 ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
45 42 , 44 syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
46 45 com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
47 46 ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
48 47 com14 88 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
49 37 , 48 syl6bi 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
50 49 com14 88 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
51 50 pm2.43i 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
52 51 com14 88 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
53 52 com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
54 32 , 53 syld 44 . . . . . . . . . . . . . . . . . . . . . . . . . 26
55 54 com13 80 . . . . . . . . . . . . . . . . . . . . . . . . 25
56 55 impcom 430 . . . . . . . . . . . . . . . . . . . . . . . 24
57 56 com23 78 . . . . . . . . . . . . . . . . . . . . . . 23
58 27 , 57 syl5bi 217 . . . . . . . . . . . . . . . . . . . . . 22
59 20 , 58 sylbid 215 . . . . . . . . . . . . . . . . . . . . 21
60 59 com23 78 . . . . . . . . . . . . . . . . . . . 20
61 60 ex 434 . . . . . . . . . . . . . . . . . . 19
62 61 adantl 466 . . . . . . . . . . . . . . . . . 18
63 62 com12 31 . . . . . . . . . . . . . . . . 17
64 63 adantlr 714 . . . . . . . . . . . . . . . 16
65 64 adantr 465 . . . . . . . . . . . . . . 15
66 eleq1 2529 . . . . . . . . . . . . . . . . . 18
67 66 ad2antlr 726 . . . . . . . . . . . . . . . . 17
68 eleq1 2529 . . . . . . . . . . . . . . . . 17
69 67 , 68 bi2anan9 873 . . . . . . . . . . . . . . . 16
70 69 anbi2d 703 . . . . . . . . . . . . . . 15
71 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
72 71 ad2antlr 726 . . . . . . . . . . . . . . . . . 18
73 fveq2 5871 . . . . . . . . . . . . . . . . . 18
74 72 , 73 eqeqan12d 2480 . . . . . . . . . . . . . . . . 17
75 simpllr 760 . . . . . . . . . . . . . . . . . 18
76 simpr 461 . . . . . . . . . . . . . . . . . 18
77 75 , 76 eqeq12d 2479 . . . . . . . . . . . . . . . . 17
78 74 , 77 imbi12d 320 . . . . . . . . . . . . . . . 16
79 78 imbi2d 316 . . . . . . . . . . . . . . 15
80 65 , 70 , 79 3imtr4d 268 . . . . . . . . . . . . . 14
81 80 ex 434 . . . . . . . . . . . . 13
82 81 rexlimdvva 2956 . . . . . . . . . . . 12
83 82 ex 434 . . . . . . . . . . 11
84 83 rexlimivv 2954 . . . . . . . . . 10
85 84 imp 429 . . . . . . . . 9
86 14 , 85 mpcom 36 . . . . . . . 8
87 86 ex 434 . . . . . . 7
88 87 com23 78 . . . . . 6
89 7 , 88 mpcom 36 . . . . 5
90 89 ralrimivv 2877 . . . 4
91 dff13 6166 . . . 4
92 5 , 90 , 91 sylanbrc 664 . . 3
93 df-f1 5598 . . . 4
94 93 simprbi 464 . . 3
95 92 , 94 syl 16 . 2
96 dff1o3 5827 . 2
97 3 , 95 , 96 sylanbrc 664 1
