Step | Hyp | Ref
| Expression |
1 | | simpll 790 |
. 2
↾t ↾t |
2 | | simpll 790 |
. . . . . . . 8
|
3 | | ssun1 3776 |
. . . . . . . . . 10
|
4 | | sseq2 3627 |
. . . . . . . . . 10
|
5 | 3, 4 | mpbiri 248 |
. . . . . . . . 9
|
6 | 5 | ad2antlr 763 |
. . . . . . . 8
|
7 | | uncmp.1 |
. . . . . . . . 9
|
8 | 7 | cmpsub 21203 |
. . . . . . . 8
↾t
|
9 | 2, 6, 8 | syl2anc 693 |
. . . . . . 7
↾t
|
10 | | simprr 796 |
. . . . . . . . 9
|
11 | 6, 10 | sseqtrd 3641 |
. . . . . . . 8
|
12 | | unieq 4444 |
. . . . . . . . . . . 12
|
13 | 12 | sseq2d 3633 |
. . . . . . . . . . 11
|
14 | | pweq 4161 |
. . . . . . . . . . . . 13
|
15 | 14 | ineq1d 3813 |
. . . . . . . . . . . 12
|
16 | 15 | rexeqdv 3145 |
. . . . . . . . . . 11
|
17 | 13, 16 | imbi12d 334 |
. . . . . . . . . 10
|
18 | 17 | rspcv 3305 |
. . . . . . . . 9
|
19 | 18 | ad2antrl 764 |
. . . . . . . 8
|
20 | 11, 19 | mpid 44 |
. . . . . . 7
|
21 | 9, 20 | sylbid 230 |
. . . . . 6
↾t |
22 | | ssun2 3777 |
. . . . . . . . . 10
|
23 | | sseq2 3627 |
. . . . . . . . . 10
|
24 | 22, 23 | mpbiri 248 |
. . . . . . . . 9
|
25 | 24 | ad2antlr 763 |
. . . . . . . 8
|
26 | 7 | cmpsub 21203 |
. . . . . . . 8
↾t
|
27 | 2, 25, 26 | syl2anc 693 |
. . . . . . 7
↾t
|
28 | 25, 10 | sseqtrd 3641 |
. . . . . . . 8
|
29 | | unieq 4444 |
. . . . . . . . . . . 12
|
30 | 29 | sseq2d 3633 |
. . . . . . . . . . 11
|
31 | | pweq 4161 |
. . . . . . . . . . . . 13
|
32 | 31 | ineq1d 3813 |
. . . . . . . . . . . 12
|
33 | 32 | rexeqdv 3145 |
. . . . . . . . . . 11
|
34 | 30, 33 | imbi12d 334 |
. . . . . . . . . 10
|
35 | 34 | rspcv 3305 |
. . . . . . . . 9
|
36 | 35 | ad2antrl 764 |
. . . . . . . 8
|
37 | 28, 36 | mpid 44 |
. . . . . . 7
|
38 | 27, 37 | sylbid 230 |
. . . . . 6
↾t |
39 | | reeanv 3107 |
. . . . . . 7
|
40 | | elin 3796 |
. . . . . . . . . . . . . . . . 17
|
41 | 40 | simplbi 476 |
. . . . . . . . . . . . . . . 16
|
42 | 41 | elpwid 4170 |
. . . . . . . . . . . . . . 15
|
43 | | elin 3796 |
. . . . . . . . . . . . . . . . 17
|
44 | 43 | simplbi 476 |
. . . . . . . . . . . . . . . 16
|
45 | 44 | elpwid 4170 |
. . . . . . . . . . . . . . 15
|
46 | 42, 45 | anim12i 590 |
. . . . . . . . . . . . . 14
|
47 | 46 | ad2antrl 764 |
. . . . . . . . . . . . 13
|
48 | | unss 3787 |
. . . . . . . . . . . . 13
|
49 | 47, 48 | sylib 208 |
. . . . . . . . . . . 12
|
50 | 40 | simprbi 480 |
. . . . . . . . . . . . . 14
|
51 | 43 | simprbi 480 |
. . . . . . . . . . . . . 14
|
52 | | unfi 8227 |
. . . . . . . . . . . . . 14
|
53 | 50, 51, 52 | syl2an 494 |
. . . . . . . . . . . . 13
|
54 | 53 | ad2antrl 764 |
. . . . . . . . . . . 12
|
55 | 49, 54 | jca 554 |
. . . . . . . . . . 11
|
56 | | elin 3796 |
. . . . . . . . . . . 12
|
57 | | vex 3203 |
. . . . . . . . . . . . . 14
|
58 | 57 | elpw2 4828 |
. . . . . . . . . . . . 13
|
59 | 58 | anbi1i 731 |
. . . . . . . . . . . 12
|
60 | 56, 59 | bitr2i 265 |
. . . . . . . . . . 11
|
61 | 55, 60 | sylib 208 |
. . . . . . . . . 10
|
62 | | simpllr 799 |
. . . . . . . . . . . . 13
|
63 | | ssun3 3778 |
. . . . . . . . . . . . . . . 16
|
64 | | ssun4 3779 |
. . . . . . . . . . . . . . . 16
|
65 | 63, 64 | anim12i 590 |
. . . . . . . . . . . . . . 15
|
66 | 65 | ad2antll 765 |
. . . . . . . . . . . . . 14
|
67 | | unss 3787 |
. . . . . . . . . . . . . 14
|
68 | 66, 67 | sylib 208 |
. . . . . . . . . . . . 13
|
69 | 62, 68 | eqsstrd 3639 |
. . . . . . . . . . . 12
|
70 | | uniun 4456 |
. . . . . . . . . . . 12
|
71 | 69, 70 | syl6sseqr 3652 |
. . . . . . . . . . 11
|
72 | | elpwi 4168 |
. . . . . . . . . . . . . . 15
|
73 | 72 | adantr 481 |
. . . . . . . . . . . . . 14
|
74 | 73 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
75 | 49, 74 | sstrd 3613 |
. . . . . . . . . . . 12
|
76 | | uniss 4458 |
. . . . . . . . . . . . 13
|
77 | 76, 7 | syl6sseqr 3652 |
. . . . . . . . . . . 12
|
78 | 75, 77 | syl 17 |
. . . . . . . . . . 11
|
79 | 71, 78 | eqssd 3620 |
. . . . . . . . . 10
|
80 | | unieq 4444 |
. . . . . . . . . . . 12
|
81 | 80 | eqeq2d 2632 |
. . . . . . . . . . 11
|
82 | 81 | rspcev 3309 |
. . . . . . . . . 10
|
83 | 61, 79, 82 | syl2anc 693 |
. . . . . . . . 9
|
84 | 83 | exp32 631 |
. . . . . . . 8
|
85 | 84 | rexlimdvv 3037 |
. . . . . . 7
|
86 | 39, 85 | syl5bir 233 |
. . . . . 6
|
87 | 21, 38, 86 | syl2and 500 |
. . . . 5
↾t
↾t
|
88 | 87 | impancom 456 |
. . . 4
↾t ↾t |
89 | 88 | expd 452 |
. . 3
↾t ↾t
|
90 | 89 | ralrimiv 2965 |
. 2
↾t ↾t
|
91 | 7 | iscmp 21191 |
. 2
|
92 | 1, 90, 91 | sylanbrc 698 |
1
↾t ↾t |