Step Hyp Ref
Expression 1 ssorduni 6367 . . . . . . . . . 10
2 1 ad2antrr 710 . . . . . . . . 9
3 nelneq 2520 . . . . . . . . . . . . . . . 16
4 elssuni 4096 . . . . . . . . . . . . . . . . . . . 20
5 4 adantl 456 . . . . . . . . . . . . . . . . . . 19
6 ssel 3327 . . . . . . . . . . . . . . . . . . . . . . 23
7 eloni 4700 . . . . . . . . . . . . . . . . . . . . . . 23
8 6 , 7 syl6 32 . . . . . . . . . . . . . . . . . . . . . 22
9 8 imp 422 . . . . . . . . . . . . . . . . . . . . 21
10 ordsseleq 4719 . . . . . . . . . . . . . . . . . . . . 21
11 9 , 1 , 10 syl2an 467 . . . . . . . . . . . . . . . . . . . 20
12 11 anabss1 795 . . . . . . . . . . . . . . . . . . 19
13 5 , 12 mpbid 204 . . . . . . . . . . . . . . . . . 18
14 13 ord 370 . . . . . . . . . . . . . . . . 17
15 14 con1d 119 . . . . . . . . . . . . . . . 16
16 3 , 15 syl5 31 . . . . . . . . . . . . . . 15
17 16 exp4b 594 . . . . . . . . . . . . . 14
18 17 pm2.43d 47 . . . . . . . . . . . . 13
19 18 com23 75 . . . . . . . . . . . 12
20 19 imp 422 . . . . . . . . . . 11
21 20 ssrdv 3339 . . . . . . . . . 10
22 ssn0 3647 . . . . . . . . . 10
23 21 , 22 sylan 461 . . . . . . . . 9
24 21 unissd 4090 . . . . . . . . . . 11
25 orduniss 4784 . . . . . . . . . . . . 13
26 1 , 25 syl 16 . . . . . . . . . . . 12
27 26 adantr 455 . . . . . . . . . . 11
28 24 , 27 eqssd 3350 . . . . . . . . . 10
29 28 adantr 455 . . . . . . . . 9
30 df-lim 4695 . . . . . . . . 9
31 2 , 23 , 29 , 30 syl3anbrc 1157 . . . . . . . 8
32 31 an32s 787 . . . . . . 7
33 32 3adantl1 1129 . . . . . 6
34 ssonuni 6368 . . . . . . . . . 10
35 limeq 4702 . . . . . . . . . . . 12
36 fveq2 5661 . . . . . . . . . . . . 13
37 iuneq1 4159 . . . . . . . . . . . . 13
38 36 , 37 eqeq12d 2436 . . . . . . . . . . . 12
39 35 , 38 imbi12d 314 . . . . . . . . . . 11
40 onfununi.1 . . . . . . . . . . 11
41 39 , 40 vtoclg 3008 . . . . . . . . . 10
42 34 , 41 syl6 32 . . . . . . . . 9
43 42 imp 422 . . . . . . . 8
44 43 3adant3 993 . . . . . . 7
45 44 adantr 455 . . . . . 6
46 33 , 45 mpd 15 . . . . 5
47 eluni2 4070 . . . . . . . . . . . 12
48 ssel 3327 . . . . . . . . . . . . . . . . . 18
49 48 anim1d 551 . . . . . . . . . . . . . . . . 17
50 onelon 4715 . . . . . . . . . . . . . . . . 17
51 49 , 50 syl6 32 . . . . . . . . . . . . . . . 16
52 48 adantrd 458 . . . . . . . . . . . . . . . 16
53 eloni 4700 . . . . . . . . . . . . . . . . . 18
54 48 , 53 syl6 32 . . . . . . . . . . . . . . . . 17
55 ordelss 4706 . . . . . . . . . . . . . . . . . 18
56 55 a1i 11 . . . . . . . . . . . . . . . . 17
57 54 , 56 syland 471 . . . . . . . . . . . . . . . 16
58 51 , 52 , 57 3jcad 1154 . . . . . . . . . . . . . . 15
59 onfununi.2 . . . . . . . . . . . . . . 15
60 58 , 59 syl6 32 . . . . . . . . . . . . . 14
61 60 exp3a 429 . . . . . . . . . . . . 13
62 61 reximdvai 2805 . . . . . . . . . . . 12
63 47 , 62 syl5bi 211 . . . . . . . . . . 11
64 ssiun 4187 . . . . . . . . . . 11
65 63 , 64 syl6 32 . . . . . . . . . 10
66 65 ralrimiv 2777 . . . . . . . . 9
67 iunss 4186 . . . . . . . . 9
68 66 , 67 sylibr 206 . . . . . . . 8
69 fveq2 5661 . . . . . . . . 9
70 69 cbviunv 4184 . . . . . . . 8
71 68 , 70 syl6sseq 3379 . . . . . . 7
72 71 3ad2ant2 995 . . . . . 6
73 72 adantr 455 . . . . 5
74 46 , 73 eqsstrd 3367 . . . 4
75 74 ex 427 . . 3
76 fveq2 5661 . . . 4
77 76 ssiun2s 4189 . . 3
78 75 , 77 pm2.61d2 155 . 2
79 34 imp 422 . . . . . 6
80 79 3adant3 993 . . . . 5
81 6 3ad2ant2 995 . . . . . 6
82 4 a1i 11 . . . . . 6
83 81 , 82 jcad 523 . . . . 5
84 sseq2 3355 . . . . . . . 8
85 84 anbi2d 688 . . . . . . 7
86 36 sseq2d 3361 . . . . . . 7
87 85 , 86 imbi12d 314 . . . . . 6
88 59 3com12 1176 . . . . . . 7
89 88 3expib 1175 . . . . . 6
90 87 , 89 vtoclga 3014 . . . . 5
91 80 , 83 , 90 sylsyld 55 . . . 4
92 91 ralrimiv 2777 . . 3
93 iunss 4186 . . 3
94 92 , 93 sylibr 206 . 2
95 78 , 94 eqssd 3350 1
