Step Hyp Ref
Expression
1 ssorduni 6621
. . . . . . . . . 10
2 1 ad2antrr 725
. . . . . . . . 9
3 nelneq 2574
. . . . . . . . . . . . . . . 16
4 elssuni 4279
. . . . . . . . . . . . . . . . . . . 20
5 4 adantl 466
. . . . . . . . . . . . . . . . . . 19
6 ssel 3497
. . . . . . . . . . . . . . . . . . . . . . 23
7 eloni 4893
. . . . . . . . . . . . . . . . . . . . . . 23
8 6 , 7 syl6 33
. . . . . . . . . . . . . . . . . . . . . 22
9 8 imp 429
. . . . . . . . . . . . . . . . . . . . 21
10 ordsseleq 4912
. . . . . . . . . . . . . . . . . . . . 21
11 9 , 1 , 10 syl2an 477
. . . . . . . . . . . . . . . . . . . 20
12 11 anabss1 814
. . . . . . . . . . . . . . . . . . 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 3509
. . . . . . . . . 10
22 ssn0 3818
. . . . . . . . . 10
23 21 , 22 sylan 471
. . . . . . . . 9
24 21 unissd 4273
. . . . . . . . . . 11
25 orduniss 4977
. . . . . . . . . . . . 13
26 1 , 25 syl 16
. . . . . . . . . . . 12
27 26 adantr 465
. . . . . . . . . . 11
28 24 , 27 eqssd 3520
. . . . . . . . . 10
29 28 adantr 465
. . . . . . . . 9
30 df-lim 4888
. . . . . . . . 9
31 2 , 23 , 29 , 30 syl3anbrc 1180
. . . . . . . 8
32 31 an32s 804
. . . . . . 7
33 32 3adantl1 1152
. . . . . 6
34 ssonuni 6622
. . . . . . . . . 10
35 limeq 4895
. . . . . . . . . . . 12
36 fveq2 5871
. . . . . . . . . . . . 13
37 iuneq1 4344
. . . . . . . . . . . . 13
38 36 , 37 eqeq12d 2479
. . . . . . . . . . . 12
39 35 , 38 imbi12d 320
. . . . . . . . . . 11
40 onfununi.1
. . . . . . . . . . 11
41 39 , 40 vtoclg 3167
. . . . . . . . . 10
42 34 , 41 syl6 33
. . . . . . . . 9
43 42 imp 429
. . . . . . . 8
44 43 3adant3 1016
. . . . . . 7
45 44 adantr 465
. . . . . 6
46 33 , 45 mpd 15
. . . . 5
47 eluni2 4253
. . . . . . . . . . . 12
48 ssel 3497
. . . . . . . . . . . . . . . . . 18
49 48 anim1d 564
. . . . . . . . . . . . . . . . 17
50 onelon 4908
. . . . . . . . . . . . . . . . 17
51 49 , 50 syl6 33
. . . . . . . . . . . . . . . 16
52 48 adantrd 468
. . . . . . . . . . . . . . . 16
53 eloni 4893
. . . . . . . . . . . . . . . . . 18
54 48 , 53 syl6 33
. . . . . . . . . . . . . . . . 17
55 ordelss 4899
. . . . . . . . . . . . . . . . . 18
56 55 a1i 11
. . . . . . . . . . . . . . . . 17
57 54 , 56 syland 481
. . . . . . . . . . . . . . . 16
58 51 , 52 , 57 3jcad 1177
. . . . . . . . . . . . . . 15
59 onfununi.2
. . . . . . . . . . . . . . 15
60 58 , 59 syl6 33
. . . . . . . . . . . . . 14
61 60 expd 436
. . . . . . . . . . . . 13
62 61 reximdvai 2929
. . . . . . . . . . . 12
63 47 , 62 syl5bi 217
. . . . . . . . . . 11
64 ssiun 4372
. . . . . . . . . . 11
65 63 , 64 syl6 33
. . . . . . . . . 10
66 65 ralrimiv 2869
. . . . . . . . 9
67 iunss 4371
. . . . . . . . 9
68 66 , 67 sylibr 212
. . . . . . . 8
69 fveq2 5871
. . . . . . . . 9
70 69 cbviunv 4369
. . . . . . . 8
71 68 , 70 syl6sseq 3549
. . . . . . 7
72 71 3ad2ant2 1018
. . . . . 6
73 72 adantr 465
. . . . 5
74 46 , 73 eqsstrd 3537
. . . 4
75 74 ex 434
. . 3
76 fveq2 5871
. . . 4
77 76 ssiun2s 4374
. . 3
78 75 , 77 pm2.61d2 160
. 2
79 34 imp 429
. . . . . 6
80 79 3adant3 1016
. . . . 5
81 6 3ad2ant2 1018
. . . . . 6
82 4 a1i 11
. . . . . 6
83 81 , 82 jcad 533
. . . . 5
84 sseq2 3525
. . . . . . . 8
85 84 anbi2d 703
. . . . . . 7
86 36 sseq2d 3531
. . . . . . 7
87 85 , 86 imbi12d 320
. . . . . 6
88 59 3com12 1200
. . . . . . 7
89 88 3expib 1199
. . . . . 6
90 87 , 89 vtoclga 3173
. . . . 5
91 80 , 83 , 90 sylsyld 56
. . . 4
92 91 ralrimiv 2869
. . 3
93 iunss 4371
. . 3
94 92 , 93 sylibr 212
. 2
95 78 , 94 eqssd 3520
1