Step Hyp Ref
Expression 1 oveq2 6304 . . . . 5
2 1 eleq2d 2527 . . . 4
3 2 imbi2d 316 . . 3
4 oveq2 6304 . . . . 5
5 4 eleq2d 2527 . . . 4
6 5 imbi2d 316 . . 3
7 oveq2 6304 . . . . 5
8 7 eleq2d 2527 . . . 4
9 8 imbi2d 316 . . 3
10 oveq2 6304 . . . . 5
11 10 eleq2d 2527 . . . 4
12 11 imbi2d 316 . . 3
13 eldifi 3625 . . . . . . . 8
14 oecl 7206 . . . . . . . 8
15 13 , 14 sylan 471 . . . . . . 7
16 om1 7210 . . . . . . 7
17 15 , 16 syl 16 . . . . . 6
18 ondif2 7171 . . . . . . . . 9
19 18 simprbi 464 . . . . . . . 8
20 19 adantr 465 . . . . . . 7
21 13 adantr 465 . . . . . . . 8
22 simpr 461 . . . . . . . . 9
23 dif20el 7174 . . . . . . . . . 10
24 23 adantr 465 . . . . . . . . 9
25 oen0 7254 . . . . . . . . 9
26 21 , 22 , 24 , 25 syl21anc 1227 . . . . . . . 8
27 omordi 7234 . . . . . . . 8
28 21 , 15 , 26 , 27 syl21anc 1227 . . . . . . 7
29 20 , 28 mpd 15 . . . . . 6
30 17 , 29 eqeltrrd 2546 . . . . 5
31 oesuc 7196 . . . . . 6
32 13 , 31 sylan 471 . . . . 5
33 30 , 32 eleqtrrd 2548 . . . 4
34 33 expcom 435 . . 3
35 oecl 7206 . . . . . . . . . . 11
36 13 , 35 sylan 471 . . . . . . . . . 10
37 om1 7210 . . . . . . . . . 10
38 36 , 37 syl 16 . . . . . . . . 9
39 19 adantr 465 . . . . . . . . . 10
40 13 adantr 465 . . . . . . . . . . 11
41 simpr 461 . . . . . . . . . . . 12
42 23 adantr 465 . . . . . . . . . . . 12
43 oen0 7254 . . . . . . . . . . . 12
44 40 , 41 , 42 , 43 syl21anc 1227 . . . . . . . . . . 11
45 omordi 7234 . . . . . . . . . . 11
46 40 , 36 , 44 , 45 syl21anc 1227 . . . . . . . . . 10
47 39 , 46 mpd 15 . . . . . . . . 9
48 38 , 47 eqeltrrd 2546 . . . . . . . 8
49 oesuc 7196 . . . . . . . . 9
50 13 , 49 sylan 471 . . . . . . . 8
51 48 , 50 eleqtrrd 2548 . . . . . . 7
52 suceloni 6648 . . . . . . . . 9
53 oecl 7206 . . . . . . . . 9
54 13 , 52 , 53 syl2an 477 . . . . . . . 8
55 ontr1 4929 . . . . . . . 8
56 54 , 55 syl 16 . . . . . . 7
57 51 , 56 mpan2d 674 . . . . . 6
58 57 expcom 435 . . . . 5
59 58 adantr 465 . . . 4
60 59 a2d 26 . . 3
61 bi2.04 361 . . . . . 6
62 61 ralbii 2888 . . . . 5
63 r19.21v 2862 . . . . 5
64 62 , 63 bitri 249 . . . 4
65 limsuc 6684 . . . . . . . . . 10
66 65 biimpa 484 . . . . . . . . 9
67 elex 3118 . . . . . . . . . . . . 13
68 sucexb 6644 . . . . . . . . . . . . . 14
69 sucidg 4961 . . . . . . . . . . . . . 14
70 68 , 69 sylbir 213 . . . . . . . . . . . . 13
71 67 , 70 syl 16 . . . . . . . . . . . 12
72 eleq2 2530 . . . . . . . . . . . . . 14
73 oveq2 6304 . . . . . . . . . . . . . . 15
74 73 eleq2d 2527 . . . . . . . . . . . . . 14
75 72 , 74 imbi12d 320 . . . . . . . . . . . . 13
76 75 rspcv 3206 . . . . . . . . . . . 12
77 71 , 76 mpid 41 . . . . . . . . . . 11
78 77 anc2li 557 . . . . . . . . . 10
79 74 rspcev 3210 . . . . . . . . . . 11
80 eliun 4335 . . . . . . . . . . 11
81 79 , 80 sylibr 212 . . . . . . . . . 10
82 78 , 81 syl6 33 . . . . . . . . 9
83 66 , 82 syl 16 . . . . . . . 8
84 83 adantr 465 . . . . . . 7
85 13 adantl 466 . . . . . . . . . 10
86 simpl 457 . . . . . . . . . 10
87 23 adantl 466 . . . . . . . . . 10
88 vex 3112 . . . . . . . . . . 11
89 oelim 7203 . . . . . . . . . . 11
90 88 , 89 mpanlr1 686 . . . . . . . . . 10
91 85 , 86 , 87 , 90 syl21anc 1227 . . . . . . . . 9
92 91 adantlr 714 . . . . . . . 8
93 92 eleq2d 2527 . . . . . . 7
94 84 , 93 sylibrd 234 . . . . . 6
95 94 ex 434 . . . . 5
96 95 a2d 26 . . . 4
97 64 , 96 syl5bi 217 . . 3
98 3 , 6 , 9 , 12 , 34 , 60 , 97 tfindsg2 6696 . 2
99 98 impancom 440 1
