Step Hyp Ref
Expression 1 brdomi 7547 . . . . 5
2 1 adantl 466 . . . 4
3 reldom 7542 . . . . . 6
4 3 brrelex2i 5046 . . . . 5
5 omelon2 6712 . . . . . . . . . . 11
6 5 ad2antlr 726 . . . . . . . . . 10
7 pwexg 4636 . . . . . . . . . . . . . 14
8 7 ad2antrr 725 . . . . . . . . . . . . 13
9 inex1g 4595 . . . . . . . . . . . . 13
10 8 , 9 syl 16 . . . . . . . . . . . 12
11 difss 3630 . . . . . . . . . . . 12
12 ssdomg 7581 . . . . . . . . . . . 12
13 10 , 11 , 12 mpisyl 18 . . . . . . . . . . 11
14 f1f1orn 5832 . . . . . . . . . . . . . . 15
15 14 adantl 466 . . . . . . . . . . . . . 14
16 f1opwfi 7844 . . . . . . . . . . . . . 14
17 15 , 16 syl 16 . . . . . . . . . . . . 13
18 f1oeng 7554 . . . . . . . . . . . . 13
19 10 , 17 , 18 syl2anc 661 . . . . . . . . . . . 12
20 pwexg 4636 . . . . . . . . . . . . . . . 16
21 20 ad2antlr 726 . . . . . . . . . . . . . . 15
22 inex1g 4595 . . . . . . . . . . . . . . 15
23 21 , 22 syl 16 . . . . . . . . . . . . . 14
24 f1f 5786 . . . . . . . . . . . . . . . . . 18
25 24 adantl 466 . . . . . . . . . . . . . . . . 17
26 frn 5742 . . . . . . . . . . . . . . . . 17
27 25 , 26 syl 16 . . . . . . . . . . . . . . . 16
28 sspwb 4701 . . . . . . . . . . . . . . . 16
29 27 , 28 sylib 196 . . . . . . . . . . . . . . 15
30 ssrin 3722 . . . . . . . . . . . . . . 15
31 29 , 30 syl 16 . . . . . . . . . . . . . 14
32 ssdomg 7581 . . . . . . . . . . . . . 14
33 23 , 31 , 32 sylc 60 . . . . . . . . . . . . 13
34 sneq 4039 . . . . . . . . . . . . . . . . . . . 20
35 pweq 4015 . . . . . . . . . . . . . . . . . . . 20
36 34 , 35 xpeq12d 5029 . . . . . . . . . . . . . . . . . . 19
37 36 cbviunv 4369 . . . . . . . . . . . . . . . . . 18
38 iuneq1 4344 . . . . . . . . . . . . . . . . . 18
39 37 , 38 syl5eq 2510 . . . . . . . . . . . . . . . . 17
40 39 fveq2d 5875 . . . . . . . . . . . . . . . 16
41 40 cbvmptv 4543 . . . . . . . . . . . . . . 15
42 41 ackbij1 8639 . . . . . . . . . . . . . 14
43 f1oeng 7554 . . . . . . . . . . . . . 14
44 23 , 42 , 43 sylancl 662 . . . . . . . . . . . . 13
45 domentr 7594 . . . . . . . . . . . . 13
46 33 , 44 , 45 syl2anc 661 . . . . . . . . . . . 12
47 endomtr 7593 . . . . . . . . . . . 12
48 19 , 46 , 47 syl2anc 661 . . . . . . . . . . 11
49 domtr 7588 . . . . . . . . . . 11
50 13 , 48 , 49 syl2anc 661 . . . . . . . . . 10
51 ondomen 8439 . . . . . . . . . 10
52 6 , 50 , 51 syl2anc 661 . . . . . . . . 9
53 eqid 2457 . . . . . . . . . . 11
54 53 fifo 7912 . . . . . . . . . 10
55 54 ad2antrr 725 . . . . . . . . 9
56 fodomnum 8459 . . . . . . . . 9
57 52 , 55 , 56 sylc 60 . . . . . . . 8
58 domtr 7588 . . . . . . . 8
59 57 , 50 , 58 syl2anc 661 . . . . . . 7
60 59 ex 434 . . . . . 6
61 60 exlimdv 1724 . . . . 5
62 4 , 61 sylan2 474 . . . 4
63 2 , 62 mpd 15 . . 3
64 63 ex 434 . 2
65 fvex 5881 . . . 4
66 ssfii 7899 . . . 4
67 ssdomg 7581 . . . 4
68 65 , 66 , 67 mpsyl 63 . . 3
69 domtr 7588 . . . 4
70 69 ex 434 . . 3
71 68 , 70 syl 16 . 2
72 64 , 71 impbid 191 1
