Step Hyp Ref
Expression 1 r0weon.1 . . . . 5
2 fveq2 5871 . . . . . . . . . . . 12
3 fveq2 5871 . . . . . . . . . . . 12
4 2 , 3 uneq12d 3658 . . . . . . . . . . 11
5 eqid 2457 . . . . . . . . . . 11
6 fvex 5881 . . . . . . . . . . . 12
7 fvex 5881 . . . . . . . . . . . 12
8 6 , 7 unex 6598 . . . . . . . . . . 11
9 4 , 5 , 8 fvmpt 5956 . . . . . . . . . 10
10 fveq2 5871 . . . . . . . . . . . 12
11 fveq2 5871 . . . . . . . . . . . 12
12 10 , 11 uneq12d 3658 . . . . . . . . . . 11
13 fvex 5881 . . . . . . . . . . . 12
14 fvex 5881 . . . . . . . . . . . 12
15 13 , 14 unex 6598 . . . . . . . . . . 11
16 12 , 5 , 15 fvmpt 5956 . . . . . . . . . 10
17 9 , 16 breqan12d 4467 . . . . . . . . 9
18 15 epelc 4798 . . . . . . . . 9
19 17 , 18 syl6bb 261 . . . . . . . 8
20 9 , 16 eqeqan12d 2480 . . . . . . . . 9
21 20 anbi1d 704 . . . . . . . 8
22 19 , 21 orbi12d 709 . . . . . . 7
23 22 pm5.32i 637 . . . . . 6
24 23 opabbii 4516 . . . . 5
25 1 , 24 eqtr4i 2489 . . . 4
26 xp1st 6830 . . . . . . . 8
27 xp2nd 6831 . . . . . . . 8
28 fvex 5881 . . . . . . . . . 10
29 28 elon 4892 . . . . . . . . 9
30 fvex 5881 . . . . . . . . . 10
31 30 elon 4892 . . . . . . . . 9
32 ordun 4984 . . . . . . . . 9
33 29 , 31 , 32 syl2anb 479 . . . . . . . 8
34 26 , 27 , 33 syl2anc 661 . . . . . . 7
35 28 , 30 unex 6598 . . . . . . . 8
36 35 elon 4892 . . . . . . 7
37 34 , 36 sylibr 212 . . . . . 6
38 5 , 37 fmpti 6054 . . . . 5
39 38 a1i 11 . . . 4
40 epweon 6619 . . . . 5
41 40 a1i 11 . . . 4
42 leweon.1 . . . . . 6
43 42 leweon 8410 . . . . 5
44 43 a1i 11 . . . 4
45 vex 3112 . . . . . . . 8
46 45 dmex 6733 . . . . . . 7
47 45 rnex 6734 . . . . . . 7
48 46 , 47 unex 6598 . . . . . 6
49 imadmres 5504 . . . . . . 7
50 inss2 3718 . . . . . . . . . 10
51 ssun1 3666 . . . . . . . . . . . . . 14
52 50 sseli 3499 . . . . . . . . . . . . . . . . 17
53 1st2nd2 6837 . . . . . . . . . . . . . . . . 17
54 52 , 53 syl 16 . . . . . . . . . . . . . . . 16
55 inss1 3717 . . . . . . . . . . . . . . . . 17
56 55 sseli 3499 . . . . . . . . . . . . . . . 16
57 54 , 56 eqeltrrd 2546 . . . . . . . . . . . . . . 15
58 28 , 30 opeldm 5211 . . . . . . . . . . . . . . 15
59 57 , 58 syl 16 . . . . . . . . . . . . . 14
60 51 , 59 sseldi 3501 . . . . . . . . . . . . 13
61 ssun2 3667 . . . . . . . . . . . . . 14
62 28 , 30 opelrn 5239 . . . . . . . . . . . . . . 15
63 57 , 62 syl 16 . . . . . . . . . . . . . 14
64 61 , 63 sseldi 3501 . . . . . . . . . . . . 13
65 prssi 4186 . . . . . . . . . . . . 13
66 60 , 64 , 65 syl2anc 661 . . . . . . . . . . . 12
67 52 , 26 syl 16 . . . . . . . . . . . . 13
68 52 , 27 syl 16 . . . . . . . . . . . . 13
69 ordunpr 6661 . . . . . . . . . . . . 13
70 67 , 68 , 69 syl2anc 661 . . . . . . . . . . . 12
71 66 , 70 sseldd 3504 . . . . . . . . . . 11
72 71 rgen 2817 . . . . . . . . . 10
73 ssrab 3577 . . . . . . . . . 10
74 50 , 72 , 73 mpbir2an 920 . . . . . . . . 9
75 dmres 5299 . . . . . . . . . 10
76 38 fdmi 5741 . . . . . . . . . . 11
77 76 ineq2i 3696 . . . . . . . . . 10
78 75 , 77 eqtri 2486 . . . . . . . . 9
79 5 mptpreima 5505 . . . . . . . . 9
80 74 , 78 , 79 3sstr4i 3542 . . . . . . . 8
81 funmpt 5629 . . . . . . . . 9
82 resss 5302 . . . . . . . . . 10
83 dmss 5207 . . . . . . . . . 10
84 82 , 83 ax-mp 5 . . . . . . . . 9
85 funimass3 6003 . . . . . . . . 9
86 81 , 84 , 85 mp2an 672 . . . . . . . 8
87 80 , 86 mpbir 209 . . . . . . 7
88 49 , 87 eqsstr3i 3534 . . . . . 6
89 48 , 88 ssexi 4597 . . . . 5
90 89 a1i 11 . . . 4
91 25 , 39 , 41 , 44 , 90 fnwe 6916 . . 3
92 epse 4867 . . . . 5
93 92 a1i 11 . . . 4
94 45 uniex 6596 . . . . . . . 8
95 94 pwex 4635 . . . . . . 7
96 95 , 95 xpex 6604 . . . . . 6
97 5 mptpreima 5505 . . . . . . . 8
98 df-rab 2816 . . . . . . . 8
99 97 , 98 eqtri 2486 . . . . . . 7
100 53 adantr 465 . . . . . . . . 9
101 elssuni 4279 . . . . . . . . . . . . 13
102 101 adantl 466 . . . . . . . . . . . 12
103 102 unssad 3680 . . . . . . . . . . 11
104 28 elpw 4018 . . . . . . . . . . 11
105 103 , 104 sylibr 212 . . . . . . . . . 10
106 102 unssbd 3681 . . . . . . . . . . 11
107 30 elpw 4018 . . . . . . . . . . 11
108 106 , 107 sylibr 212 . . . . . . . . . 10
109 105 , 108 jca 532 . . . . . . . . 9
110 elxp6 6832 . . . . . . . . 9
111 100 , 109 ,
110 sylanbrc 664 . . . . . . . 8
112 111 abssi 3574 . . . . . . 7
113 99 , 112 eqsstri 3533 . . . . . 6
114 96 , 113 ssexi 4597 . . . . 5
115 114 a1i 11 . . . 4
116 25 , 39 , 93 , 115 fnse 6917 . . 3
117 91 , 116 jca 532 . 2
118 117 trud 1404 1
