Step Hyp Ref
Expression 1 vex 3112 . . . . . . . . . 10
2 1 elixp 7496 . . . . . . . . 9
3 2 simprbi 464 . . . . . . . 8
4 ssiun2 4373 . . . . . . . . . 10
5 4 sseld 3502 . . . . . . . . 9
6 5 ralimia 2848 . . . . . . . 8
7 3 , 6 syl 16 . . . . . . 7
8 nfv 1707 . . . . . . . 8
9 nfiu1 4360 . . . . . . . . 9
10 9 nfel2 2637 . . . . . . . 8
11 fveq2 5871 . . . . . . . . 9
12 11 eleq1d 2526 . . . . . . . 8
13 8 , 10 , 12 cbvral 3080 . . . . . . 7
14 7 , 13 sylib 196 . . . . . 6
15 14 adantl 466 . . . . 5
16 15 ralrimiva 2871 . . . 4
17 eqid 2457 . . . . 5
18 17 fmpt2 6867 . . . 4
19 16 , 18 sylib 196 . . 3
20 ixpssmap2g 7518 . . . . . 6
21 20 3ad2ant2 1018 . . . . 5
22 ovex 6324 . . . . . 6
23 22 ssex 4596 . . . . 5
24 21 , 23 syl 16 . . . 4
25 simp1 996 . . . 4
26 xpexg 6602 . . . 4
27 24 , 25 , 26 syl2anc 661 . . 3
28 simp2 997 . . 3
29 fex2 6755 . . 3
30 19 , 27 , 28 , 29 syl3anc 1228 . 2
31 ffn 5736 . . . . 5
32 19 , 31 syl 16 . . . 4
33 dffn4 5806 . . . 4
34 32 , 33 sylib 196 . . 3
35 n0 3794 . . . . . . . . . 10
36 eliun 4335 . . . . . . . . . . . 12
37 nfixp1 7509 . . . . . . . . . . . . . 14
38 37 nfel2 2637 . . . . . . . . . . . . 13
39 nfv 1707 . . . . . . . . . . . . . 14
40 37 , 39 nfrex 2920 . . . . . . . . . . . . 13
41 simplrr 762 . . . . . . . . . . . . . . . . . . . 20
42 iftrue 3947 . . . . . . . . . . . . . . . . . . . . 21
43 csbeq1a 3443 . . . . . . . . . . . . . . . . . . . . . . 23
44 43 equcoms 1795 . . . . . . . . . . . . . . . . . . . . . 22
45 44 eqcomd 2465 . . . . . . . . . . . . . . . . . . . . 21
46 42 , 45 eleq12d 2539 . . . . . . . . . . . . . . . . . . . 20
47 41 , 46 syl5ibrcom 222 . . . . . . . . . . . . . . . . . . 19
48 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . 25
49 48 elixp 7496 . . . . . . . . . . . . . . . . . . . . . . . 24
50 49 simprbi 464 . . . . . . . . . . . . . . . . . . . . . . 23
51 50 adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
52 nfv 1707 . . . . . . . . . . . . . . . . . . . . . . 23
53 nfcsb1v 3450 . . . . . . . . . . . . . . . . . . . . . . . 24
54 53 nfel2 2637 . . . . . . . . . . . . . . . . . . . . . . 23
55 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . 24
56 55 , 43 eleq12d 2539 . . . . . . . . . . . . . . . . . . . . . . 23
57 52 , 54 , 56 cbvral 3080 . . . . . . . . . . . . . . . . . . . . . 22
58 51 , 57 sylib 196 . . . . . . . . . . . . . . . . . . . . 21
59 58 r19.21bi 2826 . . . . . . . . . . . . . . . . . . . 20
60 iffalse 3950 . . . . . . . . . . . . . . . . . . . . 21
61 60 eleq1d 2526 . . . . . . . . . . . . . . . . . . . 20
62 59 , 61 syl5ibrcom 222 . . . . . . . . . . . . . . . . . . 19
63 47 , 62 pm2.61d 158 . . . . . . . . . . . . . . . . . 18
64 63 ralrimiva 2871 . . . . . . . . . . . . . . . . 17
65 ixpfn 7495 . . . . . . . . . . . . . . . . . . . . 21
66 65 adantr 465 . . . . . . . . . . . . . . . . . . . 20
67 fndm 5685 . . . . . . . . . . . . . . . . . . . 20
68 66 , 67 syl 16 . . . . . . . . . . . . . . . . . . 19
69 48 dmex 6733 . . . . . . . . . . . . . . . . . . 19
70 68 , 69 syl6eqelr 2554 . . . . . . . . . . . . . . . . . 18
71 mptelixpg 7526 . . . . . . . . . . . . . . . . . 18
72 70 , 71 syl 16 . . . . . . . . . . . . . . . . 17
73 64 , 72 mpbird 232 . . . . . . . . . . . . . . . 16
74 nfcv 2619 . . . . . . . . . . . . . . . . 17
75 74 , 53 , 43 cbvixp 7506 . . . . . . . . . . . . . . . 16
76 73 , 75 syl6eleqr 2556 . . . . . . . . . . . . . . 15
77 simprl 756 . . . . . . . . . . . . . . 15
78 eqid 2457 . . . . . . . . . . . . . . . . . 18
79 vex 3112 . . . . . . . . . . . . . . . . . 18
80 42 , 78 , 79 fvmpt 5956 . . . . . . . . . . . . . . . . 17
81 80 ad2antrl 727 . . . . . . . . . . . . . . . 16
82 81 eqcomd 2465 . . . . . . . . . . . . . . 15
83 fveq1 5870 . . . . . . . . . . . . . . . . 17
84 83 eqeq2d 2471 . . . . . . . . . . . . . . . 16
85 fveq2 5871 . . . . . . . . . . . . . . . . 17
86 85 eqeq2d 2471 . . . . . . . . . . . . . . . 16
87 84 , 86 rspc2ev 3221 . . . . . . . . . . . . . . 15
88 76 , 77 , 82 , 87 syl3anc 1228 . . . . . . . . . . . . . 14
89 88 exp32 605 . . . . . . . . . . . . 13
90 38 , 40 , 89 rexlimd 2941 . . . . . . . . . . . 12
91 36 , 90 syl5bi 217 . . . . . . . . . . 11
92 91 exlimiv 1722 . . . . . . . . . 10
93 35 , 92 sylbi 195 . . . . . . . . 9
94 93 3ad2ant3 1019 . . . . . . . 8
95 94 alrimiv 1719 . . . . . . 7
96 ssab 3569 . . . . . . 7
97 95 , 96 sylibr 212 . . . . . 6
98 17 rnmpt2 6412 . . . . . 6
99 97 , 98 syl6sseqr 3550 . . . . 5
100 frn 5742 . . . . . 6
101 19 , 100 syl 16 . . . . 5
102 99 , 101 eqssd 3520 . . . 4
103 foeq3 5798 . . . 4
104 102 , 103 syl 16 . . 3
105 34 , 104 mpbird 232 . 2
106 fowdom 8018 . 2
107 30 , 105 , 106 syl2anc 661 1
