Step Hyp Ref
Expression 1 oveq2 6304 . . 3
2 breq2 4456 . . . . 5
3 2 anbi2d 703 . . . 4
4 3 abbidv 2593 . . 3
5 1 , 4 breq12d 4465 . 2
6 simpl2 1000 . . . . . . . . . 10
7 reldom 7542 . . . . . . . . . . 11
8 7 brrelexi 5045 . . . . . . . . . 10
9 6 , 8 syl 16 . . . . . . . . 9
10 7 brrelex2i 5046 . . . . . . . . . 10
11 6 , 10 syl 16 . . . . . . . . 9
12 xpcomeng 7629 . . . . . . . . 9
13 9 , 11 , 12 syl2anc 661 . . . . . . . 8
14 simpl3 1001 . . . . . . . . . 10
15 simpr 461 . . . . . . . . . . 11
16 mapdom3 7709 . . . . . . . . . . 11
17 11 , 9 , 15 , 16 syl3anc 1228 . . . . . . . . . 10
18 numdom 8440 . . . . . . . . . 10
19 14 , 17 , 18 syl2anc 661 . . . . . . . . 9
20 simpl1 999 . . . . . . . . 9
21 infxpabs 8613 . . . . . . . . 9
22 19 , 20 , 15 , 6 , 21 syl22anc 1229 . . . . . . . 8
23 entr 7587 . . . . . . . 8
24 13 , 22 , 23 syl2anc 661 . . . . . . 7
25 ssenen 7711 . . . . . . 7
26 24 , 25 syl 16 . . . . . 6
27 relen 7541 . . . . . . 7
28 27 brrelexi 5045 . . . . . 6
29 26 , 28 syl 16 . . . . 5
30 abid2 2597 . . . . . 6
31 elmapi 7460 . . . . . . . 8
32 fssxp 5748 . . . . . . . . 9
33 ffun 5738 . . . . . . . . . . 11
34 vex 3112 . . . . . . . . . . . 12
35 34 fundmen 7609 . . . . . . . . . . 11
36 ensym 7584 . . . . . . . . . . 11
37 33 , 35 , 36 3syl 20 . . . . . . . . . 10
38 fdm 5740 . . . . . . . . . 10
39 37 , 38 breqtrd 4476 . . . . . . . . 9
40 32 , 39 jca 532 . . . . . . . 8
41 31 , 40 syl 16 . . . . . . 7
42 41 ss2abi 3571 . . . . . 6
43 30 , 42 eqsstr3i 3534 . . . . 5
44 ssdomg 7581 . . . . 5
45 29 , 43 , 44 mpisyl 18 . . . 4
46 domentr 7594 . . . 4
47 45 , 26 , 46 syl2anc 661 . . 3
48 ovex 6324 . . . . . . 7
49 48 mptex 6143 . . . . . 6
50 49 rnex 6734 . . . . 5
51 ensym 7584 . . . . . . . . . . . 12
52 51 ad2antll 728 . . . . . . . . . . 11
53 bren 7545 . . . . . . . . . . 11
54 52 , 53 sylib 196 . . . . . . . . . 10
55 f1of 5821 . . . . . . . . . . . . . . . 16
56 55 adantl 466 . . . . . . . . . . . . . . 15
57 simplrl 761 . . . . . . . . . . . . . . 15
58 56 , 57 fssd 5745 . . . . . . . . . . . . . 14
59 11 , 9 elmapd 7453 . . . . . . . . . . . . . . 15
60 59 ad2antrr 725 . . . . . . . . . . . . . 14
61 58 , 60 mpbird 232 . . . . . . . . . . . . 13
62 f1ofo 5828 . . . . . . . . . . . . . . . 16
63 forn 5803 . . . . . . . . . . . . . . . 16
64 62 , 63 syl 16 . . . . . . . . . . . . . . 15
65 64 adantl 466 . . . . . . . . . . . . . 14
66 65 eqcomd 2465 . . . . . . . . . . . . 13
67 61 , 66 jca 532 . . . . . . . . . . . 12
68 67 ex 434 . . . . . . . . . . 11
69 68 eximdv 1710 . . . . . . . . . 10
70 54 , 69 mpd 15 . . . . . . . . 9
71 df-rex 2813 . . . . . . . . 9
72 70 , 71 sylibr 212 . . . . . . . 8
73 72 ex 434 . . . . . . 7
74 73 ss2abdv 3572 . . . . . 6
75 eqid 2457 . . . . . . 7
76 75 rnmpt 5253 . . . . . 6
77 74 , 76 syl6sseqr 3550 . . . . 5
78 ssdomg 7581 . . . . 5
79 50 , 77 , 78 mpsyl 63 . . . 4
80 vex 3112 . . . . . . . . 9
81 80 rnex 6734 . . . . . . . 8
82 81 rgenw 2818 . . . . . . 7
83 75 fnmpt 5712 . . . . . . 7
84 82 , 83 mp1i 12 . . . . . 6
85 dffn4 5806 . . . . . 6
86 84 , 85 sylib 196 . . . . 5
87 fodomnum 8459 . . . . 5
88 14 , 86 , 87 sylc 60 . . . 4
89 domtr 7588 . . . 4
90 79 , 88 , 89 syl2anc 661 . . 3
91 sbth 7657 . . 3
92 47 , 90 , 91 syl2anc 661 . 2
93 7 brrelex2i 5046 . . . . 5
94 93 3ad2ant1 1017 . . . 4
95 map0e 7476 . . . 4
96 94 , 95 syl 16 . . 3
97 1onn 7307 . . . . . 6
98 97 elexi 3119 . . . . 5
99 98 enref 7568 . . . 4
100 df-sn 4030 . . . . 5
101 df1o2 7161 . . . . 5
102 en0 7598 . . . . . . . 8
103 102 anbi2i 694 . . . . . . 7
104 0ss 3814 . . . . . . . . 9
105 sseq1 3524 . . . . . . . . 9
106 104 , 105 mpbiri 233 . . . . . . . 8
107 106 pm4.71ri 633 . . . . . . 7
108 103 , 107 bitr4i 252 . . . . . 6
109 108 abbii 2591 . . . . 5
110 100 , 101 ,
109 3eqtr4ri 2497 . . . 4
111 99 , 110 breqtrri 4477 . . 3
112 96 , 111 syl6eqbr 4489 . 2
113 5 , 92 , 112 pm2.61ne 2772 1
