Step Hyp Ref
Expression 1 elex 3118 . 2
2 0wdom 8017 . . . . . 6
3 breq1 4455 . . . . . 6
4 2 , 3 syl5ibrcom 222 . . . . 5
5 4 imp 429 . . . 4
6 0elpw 4621 . . . . . . 7
7 f1o0 5855 . . . . . . . 8
8 f1ofo 5828 . . . . . . . 8
9 0ex 4582 . . . . . . . . 9
10 foeq1 5796 . . . . . . . . 9
11 9 , 10 spcev 3201 . . . . . . . 8
12 7 , 8 , 11 mp2b 10 . . . . . . 7
13 foeq2 5797 . . . . . . . . 9
14 13 exbidv 1714 . . . . . . . 8
15 14 rspcev 3210 . . . . . . 7
16 6 , 12 , 15 mp2an 672 . . . . . 6
17 foeq3 5798 . . . . . . . 8
18 17 exbidv 1714 . . . . . . 7
19 18 rexbidv 2968 . . . . . 6
20 16 , 19 mpbiri 233 . . . . 5
21 20 adantl 466 . . . 4
22 5 , 21 2thd 240 . . 3
23 brwdomn0 8016 . . . . 5
24 23 adantl 466 . . . 4
25 foeq1 5796 . . . . . . 7
26 25 cbvexv 2024 . . . . . 6
27 pwidg 4025 . . . . . . . . 9
28 27 ad2antrr 725 . . . . . . . 8
29 foeq2 5797 . . . . . . . . . 10
30 29 exbidv 1714 . . . . . . . . 9
31 30 rspcev 3210 . . . . . . . 8
32 28 , 31 sylancom 667 . . . . . . 7
33 32 ex 434 . . . . . 6
34 26 , 33 syl5bi 217 . . . . 5
35 n0 3794 . . . . . . . . . . 11
36 35 biimpi 194 . . . . . . . . . 10
37 36 ad2antlr 726 . . . . . . . . 9
38 vex 3112 . . . . . . . . . . . . 13
39 difexg 4600 . . . . . . . . . . . . . 14
40 snex 4693 . . . . . . . . . . . . . 14
41 xpexg 6602 . . . . . . . . . . . . . 14
42 39 , 40 , 41 sylancl 662 . . . . . . . . . . . . 13
43 unexg 6601 . . . . . . . . . . . . 13
44 38 , 42 , 43 sylancr 663 . . . . . . . . . . . 12
45 44 adantr 465 . . . . . . . . . . 11
46 45 ad2antrr 725 . . . . . . . . . 10
47 fofn 5802 . . . . . . . . . . . . . . 15
48 47 adantl 466 . . . . . . . . . . . . . 14
49 48 ad2antlr 726 . . . . . . . . . . . . 13
50 vex 3112 . . . . . . . . . . . . . 14
51 fnconstg 5778 . . . . . . . . . . . . . 14
52 50 , 51 mp1i 12 . . . . . . . . . . . . 13
53 disjdif 3900 . . . . . . . . . . . . . 14
54 53 a1i 11 . . . . . . . . . . . . 13
55 fnun 5692 . . . . . . . . . . . . 13
56 49 , 52 , 54 , 55 syl21anc 1227 . . . . . . . . . . . 12
57 elpwi 4021 . . . . . . . . . . . . . . . 16
58 undif 3908 . . . . . . . . . . . . . . . 16
59 57 , 58 sylib 196 . . . . . . . . . . . . . . 15
60 59 ad2antrl 727 . . . . . . . . . . . . . 14
61 60 adantr 465 . . . . . . . . . . . . 13
62 61 fneq2d 5677 . . . . . . . . . . . 12
63 56 , 62 mpbid 210 . . . . . . . . . . 11
64 rnun 5419 . . . . . . . . . . . 12
65 forn 5803 . . . . . . . . . . . . . . . 16
66 65 ad2antll 728 . . . . . . . . . . . . . . 15
67 66 adantr 465 . . . . . . . . . . . . . 14
68 67 uneq1d 3656 . . . . . . . . . . . . 13
69 fconst6g 5779 . . . . . . . . . . . . . . . 16
70 frn 5742 . . . . . . . . . . . . . . . 16
71 69 , 70 syl 16 . . . . . . . . . . . . . . 15
72 71 adantl 466 . . . . . . . . . . . . . 14
73 ssequn2 3676 . . . . . . . . . . . . . 14
74 72 , 73 sylib 196 . . . . . . . . . . . . 13
75 68 , 74 eqtrd 2498 . . . . . . . . . . . 12
76 64 , 75 syl5eq 2510 . . . . . . . . . . 11
77 df-fo 5599 . . . . . . . . . . 11
78 63 , 76 , 77 sylanbrc 664 . . . . . . . . . 10
79 foeq1 5796 . . . . . . . . . . 11
80 79 spcegv 3195 . . . . . . . . . 10
81 46 , 78 , 80 sylc 60 . . . . . . . . 9
82 37 , 81 exlimddv 1726 . . . . . . . 8
83 82 expr 615 . . . . . . 7
84 83 exlimdv 1724 . . . . . 6
85 84 rexlimdva 2949 . . . . 5
86 34 , 85 impbid 191 . . . 4
87 24 , 86 bitrd 253 . . 3
88 22 , 87 pm2.61dane 2775 . 2
89 1 , 88 syl 16 1
