Step | Hyp | Ref
| Expression |
1 | | suceq 4375 |
. . . . 5
|
2 | 1 | eleq1d 2233 |
. . . 4
|
3 | | tfr1onlemsucaccv.u |
. . . . 5
|
4 | 3 | ralrimiva 2537 |
. . . 4
|
5 | | tfr1onlemsucaccv.zy |
. . . . 5
|
6 | | tfr1onlemsucaccv.yx |
. . . . 5
|
7 | | elunii 3789 |
. . . . 5
|
8 | 5, 6, 7 | syl2anc 409 |
. . . 4
|
9 | 2, 4, 8 | rspcdva 2831 |
. . 3
|
10 | | tfr1on.f |
. . . 4
recs |
11 | | tfr1on.g |
. . . 4
|
12 | | tfr1on.x |
. . . 4
|
13 | | tfr1on.ex |
. . . 4
|
14 | | tfr1onlemsucfn.1 |
. . . 4
|
15 | 5, 6 | jca 304 |
. . . . 5
|
16 | | ordtr1 4361 |
. . . . 5
|
17 | 12, 15, 16 | sylc 62 |
. . . 4
|
18 | | tfr1onlemsucaccv.gfn |
. . . 4
|
19 | | tfr1onlemsucaccv.gacc |
. . . 4
|
20 | 10, 11, 12, 13, 14, 17, 18, 19 | tfr1onlemsucfn 6300 |
. . 3
|
21 | | vex 2725 |
. . . . . 6
|
22 | 21 | elsuc 4379 |
. . . . 5
|
23 | | vex 2725 |
. . . . . . . . . . 11
|
24 | 14 | tfr1onlem3ag 6297 |
. . . . . . . . . . 11
|
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . 10
|
26 | 19, 25 | sylib 121 |
. . . . . . . . 9
|
27 | | simprrr 530 |
. . . . . . . . . 10
|
28 | | simprrl 529 |
. . . . . . . . . . . 12
|
29 | 18 | adantr 274 |
. . . . . . . . . . . 12
|
30 | | fndmu 5284 |
. . . . . . . . . . . 12
|
31 | 28, 29, 30 | syl2anc 409 |
. . . . . . . . . . 11
|
32 | 31 | raleqdv 2665 |
. . . . . . . . . 10
|
33 | 27, 32 | mpbid 146 |
. . . . . . . . 9
|
34 | 26, 33 | rexlimddv 2586 |
. . . . . . . 8
|
35 | 34 | r19.21bi 2552 |
. . . . . . 7
|
36 | | ordelon 4356 |
. . . . . . . . . . . . 13
|
37 | 12, 17, 36 | syl2anc 409 |
. . . . . . . . . . . 12
|
38 | | onelon 4357 |
. . . . . . . . . . . 12
|
39 | 37, 38 | sylan 281 |
. . . . . . . . . . 11
|
40 | | eloni 4348 |
. . . . . . . . . . 11
|
41 | | ordirr 4514 |
. . . . . . . . . . 11
|
42 | 39, 40, 41 | 3syl 17 |
. . . . . . . . . 10
|
43 | | elequ2 2140 |
. . . . . . . . . . . 12
|
44 | 43 | biimpcd 158 |
. . . . . . . . . . 11
|
45 | 44 | adantl 275 |
. . . . . . . . . 10
|
46 | 42, 45 | mtod 653 |
. . . . . . . . 9
|
47 | 46 | neqned 2341 |
. . . . . . . 8
|
48 | | fvunsng 5674 |
. . . . . . . 8
|
49 | 21, 47, 48 | sylancr 411 |
. . . . . . 7
|
50 | | eloni 4348 |
. . . . . . . . . . . 12
|
51 | 37, 50 | syl 14 |
. . . . . . . . . . 11
|
52 | | ordelss 4352 |
. . . . . . . . . . 11
|
53 | 51, 52 | sylan 281 |
. . . . . . . . . 10
|
54 | | resabs1 4908 |
. . . . . . . . . 10
|
55 | 53, 54 | syl 14 |
. . . . . . . . 9
|
56 | | ordirr 4514 |
. . . . . . . . . . . . 13
|
57 | 51, 56 | syl 14 |
. . . . . . . . . . . 12
|
58 | | fsnunres 5682 |
. . . . . . . . . . . 12
|
59 | 18, 57, 58 | syl2anc 409 |
. . . . . . . . . . 11
|
60 | 59 | reseq1d 4878 |
. . . . . . . . . 10
|
61 | 60 | adantr 274 |
. . . . . . . . 9
|
62 | 55, 61 | eqtr3d 2199 |
. . . . . . . 8
|
63 | 62 | fveq2d 5485 |
. . . . . . 7
|
64 | 35, 49, 63 | 3eqtr4d 2207 |
. . . . . 6
|
65 | | fneq2 5272 |
. . . . . . . . . . . . 13
|
66 | 65 | imbi1d 230 |
. . . . . . . . . . . 12
|
67 | 66 | albidv 1811 |
. . . . . . . . . . 11
|
68 | 13 | 3expia 1194 |
. . . . . . . . . . . . 13
|
69 | 68 | alrimiv 1861 |
. . . . . . . . . . . 12
|
70 | 69 | ralrimiva 2537 |
. . . . . . . . . . 11
|
71 | 67, 70, 17 | rspcdva 2831 |
. . . . . . . . . 10
|
72 | | fneq1 5271 |
. . . . . . . . . . . 12
|
73 | | fveq2 5481 |
. . . . . . . . . . . . 13
|
74 | 73 | eleq1d 2233 |
. . . . . . . . . . . 12
|
75 | 72, 74 | imbi12d 233 |
. . . . . . . . . . 11
|
76 | 75 | spv 1847 |
. . . . . . . . . 10
|
77 | 71, 18, 76 | sylc 62 |
. . . . . . . . 9
|
78 | | fndm 5282 |
. . . . . . . . . . 11
|
79 | 18, 78 | syl 14 |
. . . . . . . . . 10
|
80 | 57, 79 | neleqtrrd 2263 |
. . . . . . . . 9
|
81 | | fsnunfv 5681 |
. . . . . . . . 9
|
82 | 5, 77, 80, 81 | syl3anc 1227 |
. . . . . . . 8
|
83 | 82 | adantr 274 |
. . . . . . 7
|
84 | | simpr 109 |
. . . . . . . 8
|
85 | 84 | fveq2d 5485 |
. . . . . . 7
|
86 | | reseq2 4874 |
. . . . . . . . 9
|
87 | 86, 59 | sylan9eqr 2219 |
. . . . . . . 8
|
88 | 87 | fveq2d 5485 |
. . . . . . 7
|
89 | 83, 85, 88 | 3eqtr4d 2207 |
. . . . . 6
|
90 | 64, 89 | jaodan 787 |
. . . . 5
|
91 | 22, 90 | sylan2b 285 |
. . . 4
|
92 | 91 | ralrimiva 2537 |
. . 3
|
93 | | fneq2 5272 |
. . . . 5
|
94 | | raleq 2659 |
. . . . 5
|
95 | 93, 94 | anbi12d 465 |
. . . 4
|
96 | 95 | rspcev 2826 |
. . 3
|
97 | 9, 20, 92, 96 | syl12anc 1225 |
. 2
|
98 | | vex 2725 |
. . . . . 6
|
99 | | opexg 4201 |
. . . . . 6
|
100 | 98, 77, 99 | sylancr 411 |
. . . . 5
|
101 | | snexg 4158 |
. . . . 5
|
102 | 100, 101 | syl 14 |
. . . 4
|
103 | | unexg 4416 |
. . . 4
|
104 | 23, 102, 103 | sylancr 411 |
. . 3
|
105 | 14 | tfr1onlem3ag 6297 |
. . 3
|
106 | 104, 105 | syl 14 |
. 2
|
107 | 97, 106 | mpbird 166 |
1
|