Step Hyp Ref
Expression 1 ssorduni 6530 . . . . . . . . . 10
2 1 ad2antrr 725 . . . . . . . . 9
3 nelneq 2571 . . . . . . . . . . . . . . . 16
4 elssuni 4238 . . . . . . . . . . . . . . . . . . . 20
5 4 adantl 466 . . . . . . . . . . . . . . . . . . 19
6 ssel 3464 . . . . . . . . . . . . . . . . . . . . . . 23
7 eloni 4846 . . . . . . . . . . . . . . . . . . . . . . 23
8 6 , 7 syl6 33 . . . . . . . . . . . . . . . . . . . . . 22
9 8 imp 429 . . . . . . . . . . . . . . . . . . . . 21
10 ordsseleq 4865 . . . . . . . . . . . . . . . . . . . . 21
11 9 , 1 , 10 syl2an 477 . . . . . . . . . . . . . . . . . . . 20
12 11 anabss1 810 . . . . . . . . . . . . . . . . . . 19
13 5 , 12 mpbid 210 . . . . . . . . . . . . . . . . . 18
14 13 ord 377 . . . . . . . . . . . . . . . . 17
15 14 con1d 124 . . . . . . . . . . . . . . . 16
16 3 , 15 syl5 32 . . . . . . . . . . . . . . 15
17 16 exp4b 607 . . . . . . . . . . . . . 14
18 17 pm2.43d 48 . . . . . . . . . . . . 13
19 18 com23 78 . . . . . . . . . . . 12
20 19 imp 429 . . . . . . . . . . 11
21 20 ssrdv 3476 . . . . . . . . . 10
22 ssn0 3784 . . . . . . . . . 10
23 21 , 22 sylan 471 . . . . . . . . 9
24 21 unissd 4232 . . . . . . . . . . 11
25 orduniss 4930 . . . . . . . . . . . . 13
26 1 , 25 syl 16 . . . . . . . . . . . 12
27 26 adantr 465 . . . . . . . . . . 11
28 24 , 27 eqssd 3487 . . . . . . . . . 10
29 28 adantr 465 . . . . . . . . 9
30 df-lim 4841 . . . . . . . . 9
31 2 , 23 , 29 , 30 syl3anbrc 1172 . . . . . . . 8
32 31 an32s 802 . . . . . . 7
33 32 3adantl1 1144 . . . . . 6
34 ssonuni 6531 . . . . . . . . . 10
35 limeq 4848 . . . . . . . . . . . 12
36 fveq2 5813 . . . . . . . . . . . . 13
37 iuneq1 4301 . . . . . . . . . . . . 13
38 36 , 37 eqeq12d 2476 . . . . . . . . . . . 12
39 35 , 38 imbi12d 320 . . . . . . . . . . 11
40 onfununi.1 . . . . . . . . . . 11
41 39 , 40 vtoclg 3139 . . . . . . . . . 10
42 34 , 41 syl6 33 . . . . . . . . 9
43 42 imp 429 . . . . . . . 8
44 43 3adant3 1008 . . . . . . 7
45 44 adantr 465 . . . . . 6
46 33 , 45 mpd 15 . . . . 5
47 eluni2 4212 . . . . . . . . . . . 12
48 ssel 3464 . . . . . . . . . . . . . . . . . 18
49 48 anim1d 564 . . . . . . . . . . . . . . . . 17
50 onelon 4861 . . . . . . . . . . . . . . . . 17
51 49 , 50 syl6 33 . . . . . . . . . . . . . . . 16
52 48 adantrd 468 . . . . . . . . . . . . . . . 16
53 eloni 4846 . . . . . . . . . . . . . . . . . 18
54 48 , 53 syl6 33 . . . . . . . . . . . . . . . . 17
55 ordelss 4852 . . . . . . . . . . . . . . . . . 18
56 55 a1i 11 . . . . . . . . . . . . . . . . 17
57 54 , 56 syland 481 . . . . . . . . . . . . . . . 16
58 51 , 52 , 57 3jcad 1169 . . . . . . . . . . . . . . 15
59 onfununi.2 . . . . . . . . . . . . . . 15
60 58 , 59 syl6 33 . . . . . . . . . . . . . 14
61 60 expd 436 . . . . . . . . . . . . 13
62 61 reximdvai 2934 . . . . . . . . . . . 12
63 47 , 62 syl5bi 217 . . . . . . . . . . 11
64 ssiun 4329 . . . . . . . . . . 11
65 63 , 64 syl6 33 . . . . . . . . . 10
66 65 ralrimiv 2829 . . . . . . . . 9
67 iunss 4328 . . . . . . . . 9
68 66 , 67 sylibr 212 . . . . . . . 8
69 fveq2 5813 . . . . . . . . 9
70 69 cbviunv 4326 . . . . . . . 8
71 68 , 70 syl6sseq 3516 . . . . . . 7
72 71 3ad2ant2 1010 . . . . . 6
73 72 adantr 465 . . . . 5
74 46 , 73 eqsstrd 3504 . . . 4
75 74 ex 434 . . 3
76 fveq2 5813 . . . 4
77 76 ssiun2s 4331 . . 3
78 75 , 77 pm2.61d2 160 . 2
79 34 imp 429 . . . . . 6
80 79 3adant3 1008 . . . . 5
81 6 3ad2ant2 1010 . . . . . 6
82 4 a1i 11 . . . . . 6
83 81 , 82 jcad 533 . . . . 5
84 sseq2 3492 . . . . . . . 8
85 84 anbi2d 703 . . . . . . 7
86 36 sseq2d 3498 . . . . . . 7
87 85 , 86 imbi12d 320 . . . . . 6
88 59 3com12 1192 . . . . . . 7
89 88 3expib 1191 . . . . . 6
90 87 , 89 vtoclga 3145 . . . . 5
91 80 , 83 , 90 sylsyld 56 . . . 4
92 91 ralrimiv 2829 . . 3
93 iunss 4328 . . 3
94 92 , 93 sylibr 212 . 2
95 78 , 94 eqssd 3487 1
