Step | Hyp | Ref
| Expression |
1 | | r0weon.1 |
. . . . 5
|
2 | | fveq2 6191 |
. . . . . . . . . . . 12
|
3 | | fveq2 6191 |
. . . . . . . . . . . 12
|
4 | 2, 3 | uneq12d 3768 |
. . . . . . . . . . 11
|
5 | | eqid 2622 |
. . . . . . . . . . 11
|
6 | | fvex 6201 |
. . . . . . . . . . . 12
|
7 | | fvex 6201 |
. . . . . . . . . . . 12
|
8 | 6, 7 | unex 6956 |
. . . . . . . . . . 11
|
9 | 4, 5, 8 | fvmpt 6282 |
. . . . . . . . . 10
|
10 | | fveq2 6191 |
. . . . . . . . . . . 12
|
11 | | fveq2 6191 |
. . . . . . . . . . . 12
|
12 | 10, 11 | uneq12d 3768 |
. . . . . . . . . . 11
|
13 | | fvex 6201 |
. . . . . . . . . . . 12
|
14 | | fvex 6201 |
. . . . . . . . . . . 12
|
15 | 13, 14 | unex 6956 |
. . . . . . . . . . 11
|
16 | 12, 5, 15 | fvmpt 6282 |
. . . . . . . . . 10
|
17 | 9, 16 | breqan12d 4669 |
. . . . . . . . 9
|
18 | 15 | epelc 5031 |
. . . . . . . . 9
|
19 | 17, 18 | syl6bb 276 |
. . . . . . . 8
|
20 | 9, 16 | eqeqan12d 2638 |
. . . . . . . . 9
|
21 | 20 | anbi1d 741 |
. . . . . . . 8
|
22 | 19, 21 | orbi12d 746 |
. . . . . . 7
|
23 | 22 | pm5.32i 669 |
. . . . . 6
|
24 | 23 | opabbii 4717 |
. . . . 5
|
25 | 1, 24 | eqtr4i 2647 |
. . . 4
|
26 | | xp1st 7198 |
. . . . . . . 8
|
27 | | xp2nd 7199 |
. . . . . . . 8
|
28 | | fvex 6201 |
. . . . . . . . . 10
|
29 | 28 | elon 5732 |
. . . . . . . . 9
|
30 | | fvex 6201 |
. . . . . . . . . 10
|
31 | 30 | elon 5732 |
. . . . . . . . 9
|
32 | | ordun 5829 |
. . . . . . . . 9
|
33 | 29, 31, 32 | syl2anb 496 |
. . . . . . . 8
|
34 | 26, 27, 33 | syl2anc 693 |
. . . . . . 7
|
35 | 28, 30 | unex 6956 |
. . . . . . . 8
|
36 | 35 | elon 5732 |
. . . . . . 7
|
37 | 34, 36 | sylibr 224 |
. . . . . 6
|
38 | 5, 37 | fmpti 6383 |
. . . . 5
|
39 | 38 | a1i 11 |
. . . 4
|
40 | | epweon 6983 |
. . . . 5
|
41 | 40 | a1i 11 |
. . . 4
|
42 | | leweon.1 |
. . . . . 6
|
43 | 42 | leweon 8834 |
. . . . 5
|
44 | 43 | a1i 11 |
. . . 4
|
45 | | vex 3203 |
. . . . . . . 8
|
46 | 45 | dmex 7099 |
. . . . . . 7
|
47 | 45 | rnex 7100 |
. . . . . . 7
|
48 | 46, 47 | unex 6956 |
. . . . . 6
|
49 | | imadmres 5627 |
. . . . . . 7
|
50 | | inss2 3834 |
. . . . . . . . . 10
|
51 | | ssun1 3776 |
. . . . . . . . . . . . . 14
|
52 | 50 | sseli 3599 |
. . . . . . . . . . . . . . . . 17
|
53 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . 17
|
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . 16
|
55 | | inss1 3833 |
. . . . . . . . . . . . . . . . 17
|
56 | 55 | sseli 3599 |
. . . . . . . . . . . . . . . 16
|
57 | 54, 56 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
|
58 | 28, 30 | opeldm 5328 |
. . . . . . . . . . . . . . 15
|
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . 14
|
60 | 51, 59 | sseldi 3601 |
. . . . . . . . . . . . 13
|
61 | | ssun2 3777 |
. . . . . . . . . . . . . 14
|
62 | 28, 30 | opelrn 5357 |
. . . . . . . . . . . . . . 15
|
63 | 57, 62 | syl 17 |
. . . . . . . . . . . . . 14
|
64 | 61, 63 | sseldi 3601 |
. . . . . . . . . . . . 13
|
65 | | prssi 4353 |
. . . . . . . . . . . . 13
|
66 | 60, 64, 65 | syl2anc 693 |
. . . . . . . . . . . 12
|
67 | 52, 26 | syl 17 |
. . . . . . . . . . . . 13
|
68 | 52, 27 | syl 17 |
. . . . . . . . . . . . 13
|
69 | | ordunpr 7026 |
. . . . . . . . . . . . 13
|
70 | 67, 68, 69 | syl2anc 693 |
. . . . . . . . . . . 12
|
71 | 66, 70 | sseldd 3604 |
. . . . . . . . . . 11
|
72 | 71 | rgen 2922 |
. . . . . . . . . 10
|
73 | | ssrab 3680 |
. . . . . . . . . 10
|
74 | 50, 72, 73 | mpbir2an 955 |
. . . . . . . . 9
|
75 | | dmres 5419 |
. . . . . . . . . 10
|
76 | 38 | fdmi 6052 |
. . . . . . . . . . 11
|
77 | 76 | ineq2i 3811 |
. . . . . . . . . 10
|
78 | 75, 77 | eqtri 2644 |
. . . . . . . . 9
|
79 | 5 | mptpreima 5628 |
. . . . . . . . 9
|
80 | 74, 78, 79 | 3sstr4i 3644 |
. . . . . . . 8
|
81 | | funmpt 5926 |
. . . . . . . . 9
|
82 | | resss 5422 |
. . . . . . . . . 10
|
83 | | dmss 5323 |
. . . . . . . . . 10
|
84 | 82, 83 | ax-mp 5 |
. . . . . . . . 9
|
85 | | funimass3 6333 |
. . . . . . . . 9
|
86 | 81, 84, 85 | mp2an 708 |
. . . . . . . 8
|
87 | 80, 86 | mpbir 221 |
. . . . . . 7
|
88 | 49, 87 | eqsstr3i 3636 |
. . . . . 6
|
89 | 48, 88 | ssexi 4803 |
. . . . 5
|
90 | 89 | a1i 11 |
. . . 4
|
91 | 25, 39, 41, 44, 90 | fnwe 7293 |
. . 3
|
92 | | epse 5097 |
. . . . 5
Se |
93 | 92 | a1i 11 |
. . . 4
Se |
94 | | vuniex 6954 |
. . . . . . . 8
|
95 | 94 | pwex 4848 |
. . . . . . 7
|
96 | 95, 95 | xpex 6962 |
. . . . . 6
|
97 | 5 | mptpreima 5628 |
. . . . . . . 8
|
98 | | df-rab 2921 |
. . . . . . . 8
|
99 | 97, 98 | eqtri 2644 |
. . . . . . 7
|
100 | 53 | adantr 481 |
. . . . . . . . 9
|
101 | | elssuni 4467 |
. . . . . . . . . . . . 13
|
102 | 101 | adantl 482 |
. . . . . . . . . . . 12
|
103 | 102 | unssad 3790 |
. . . . . . . . . . 11
|
104 | 28 | elpw 4164 |
. . . . . . . . . . 11
|
105 | 103, 104 | sylibr 224 |
. . . . . . . . . 10
|
106 | 102 | unssbd 3791 |
. . . . . . . . . . 11
|
107 | 30 | elpw 4164 |
. . . . . . . . . . 11
|
108 | 106, 107 | sylibr 224 |
. . . . . . . . . 10
|
109 | 105, 108 | jca 554 |
. . . . . . . . 9
|
110 | | elxp6 7200 |
. . . . . . . . 9
|
111 | 100, 109,
110 | sylanbrc 698 |
. . . . . . . 8
|
112 | 111 | abssi 3677 |
. . . . . . 7
|
113 | 99, 112 | eqsstri 3635 |
. . . . . 6
|
114 | 96, 113 | ssexi 4803 |
. . . . 5
|
115 | 114 | a1i 11 |
. . . 4
|
116 | 25, 39, 93, 115 | fnse 7294 |
. . 3
Se |
117 | 91, 116 | jca 554 |
. 2
Se |
118 | 117 | trud 1493 |
1
Se |