Step | Hyp | Ref
| Expression |
1 | | rabexg 4812 |
. . . . . . 7
|
2 | 1 | ad2antrr 762 |
. . . . . 6
↾t |
3 | | ssrab2 3687 |
. . . . . . 7
|
4 | | elpwg 4166 |
. . . . . . 7
|
5 | 3, 4 | mpbiri 248 |
. . . . . 6
|
6 | 2, 5 | syl 17 |
. . . . 5
↾t |
7 | | unieq 4444 |
. . . . . . . 8
|
8 | 7 | sseq2d 3633 |
. . . . . . 7
|
9 | | pweq 4161 |
. . . . . . . . 9
|
10 | 9 | ineq1d 3813 |
. . . . . . . 8
|
11 | 10 | rexeqdv 3145 |
. . . . . . 7
|
12 | 8, 11 | imbi12d 334 |
. . . . . 6
|
13 | 12 | rspcva 3307 |
. . . . 5
|
14 | 6, 13 | sylan 488 |
. . . 4
↾t
|
15 | 14 | ex 450 |
. . 3
↾t |
16 | | cmpsub.1 |
. . . . . . . 8
|
17 | 16 | restuni 20966 |
. . . . . . 7
↾t |
18 | 17 | adantr 481 |
. . . . . 6
↾t
↾t |
19 | 18 | eqeq1d 2624 |
. . . . 5
↾t ↾t |
20 | | selpw 4165 |
. . . . . . . . . . 11
↾t ↾t |
21 | | eleq2 2690 |
. . . . . . . . . . . . . . 15
|
22 | | eluni 4439 |
. . . . . . . . . . . . . . 15
|
23 | 21, 22 | syl6bb 276 |
. . . . . . . . . . . . . 14
|
24 | 23 | adantl 482 |
. . . . . . . . . . . . 13
↾t
|
25 | | ssel 3597 |
. . . . . . . . . . . . . . . . . . 19
↾t
↾t |
26 | 16 | sseq2i 3630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
27 | | uniexg 6955 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
28 | | ssexg 4804 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
29 | 28 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
30 | 27, 29 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
31 | 26, 30 | sylan2b 492 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
32 | | elrest 16088 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t
|
33 | 31, 32 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
↾t
|
34 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
35 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
36 | 34, 35 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
37 | 36 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
38 | 37 | 3ad2antl3 1225 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
39 | 38 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
40 | | simp12 1092 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
41 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
42 | 41 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
43 | 42 | 3ad2antl3 1225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
44 | 43 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
45 | | ineq1 3807 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
46 | 45 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
47 | 46 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
48 | 40, 44, 47 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
49 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
50 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
51 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
52 | 50, 51 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
53 | 49, 52 | spcev 3300 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
54 | 39, 48, 53 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
55 | 54 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
56 | 55 | rexlimdv3a 3033 |
. . . . . . . . . . . . . . . . . . . . . 22
|
57 | 33, 56 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . 21
↾t |
58 | 57 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
↾t |
59 | 58 | com4l 92 |
. . . . . . . . . . . . . . . . . . 19
↾t
|
60 | 25, 59 | sylcom 30 |
. . . . . . . . . . . . . . . . . 18
↾t
|
61 | 60 | com24 95 |
. . . . . . . . . . . . . . . . 17
↾t |
62 | 61 | impcom 446 |
. . . . . . . . . . . . . . . 16
↾t |
63 | 62 | impd 447 |
. . . . . . . . . . . . . . 15
↾t
|
64 | 63 | exlimdv 1861 |
. . . . . . . . . . . . . 14
↾t |
65 | 64 | adantr 481 |
. . . . . . . . . . . . 13
↾t
|
66 | 24, 65 | sylbid 230 |
. . . . . . . . . . . 12
↾t
|
67 | 66 | ex 450 |
. . . . . . . . . . 11
↾t
|
68 | 20, 67 | sylan2b 492 |
. . . . . . . . . 10
↾t
|
69 | 68 | imp 445 |
. . . . . . . . 9
↾t
|
70 | | eluni 4439 |
. . . . . . . . 9
|
71 | 69, 70 | syl6ibr 242 |
. . . . . . . 8
↾t
|
72 | 71 | ssrdv 3609 |
. . . . . . 7
↾t
|
73 | | pm2.27 42 |
. . . . . . . . 9
|
74 | | elin 3796 |
. . . . . . . . . . 11
|
75 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
|
76 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . 19
|
77 | 76 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . 18
|
78 | 75, 77 | elab 3350 |
. . . . . . . . . . . . . . . . 17
|
79 | | selpw 4165 |
. . . . . . . . . . . . . . . . . . . 20
|
80 | | ssel 3597 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
81 | | ineq1 3807 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
82 | 81 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
83 | 82 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
84 | | eleq1a 2696 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
85 | 84 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
86 | 83, 85 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
87 | 80, 86 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . 22
|
88 | 87 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . 21
↾t
|
89 | 88 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
↾t
|
90 | 79, 89 | sylanb 489 |
. . . . . . . . . . . . . . . . . . 19
↾t
|
91 | 90 | 3imp 1256 |
. . . . . . . . . . . . . . . . . 18
↾t
|
92 | 91 | rexlimdv 3030 |
. . . . . . . . . . . . . . . . 17
↾t
|
93 | 78, 92 | syl5bi 232 |
. . . . . . . . . . . . . . . 16
↾t
|
94 | 93 | ssrdv 3609 |
. . . . . . . . . . . . . . 15
↾t
|
95 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
96 | 95 | abrexex 7141 |
. . . . . . . . . . . . . . . 16
|
97 | 96 | elpw 4164 |
. . . . . . . . . . . . . . 15
|
98 | 94, 97 | sylibr 224 |
. . . . . . . . . . . . . 14
↾t
|
99 | | abrexfi 8266 |
. . . . . . . . . . . . . . . 16
|
100 | 99 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
101 | 100 | 3adant3 1081 |
. . . . . . . . . . . . . 14
↾t
|
102 | 98, 101 | elind 3798 |
. . . . . . . . . . . . 13
↾t
|
103 | | dfss 3589 |
. . . . . . . . . . . . . . . . 17
|
104 | 103 | biimpi 206 |
. . . . . . . . . . . . . . . 16
|
105 | | uniiun 4573 |
. . . . . . . . . . . . . . . . . 18
|
106 | 105 | ineq2i 3811 |
. . . . . . . . . . . . . . . . 17
|
107 | | iunin2 4584 |
. . . . . . . . . . . . . . . . 17
|
108 | | incom 3805 |
. . . . . . . . . . . . . . . . . . 19
|
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
110 | 109 | iuneq2i 4539 |
. . . . . . . . . . . . . . . . 17
|
111 | 106, 107,
110 | 3eqtr2i 2650 |
. . . . . . . . . . . . . . . 16
|
112 | 104, 111 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
113 | 112 | 3ad2ant2 1083 |
. . . . . . . . . . . . . 14
↾t
|
114 | 18 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
↾t
↾t |
115 | 114 | 3adant1 1079 |
. . . . . . . . . . . . . 14
↾t
↾t |
116 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
117 | 116 | inex1 4799 |
. . . . . . . . . . . . . . . 16
|
118 | 117 | dfiun2 4554 |
. . . . . . . . . . . . . . 15
|
119 | 118 | a1i 11 |
. . . . . . . . . . . . . 14
↾t
|
120 | 113, 115,
119 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
↾t
↾t
|
121 | | unieq 4444 |
. . . . . . . . . . . . . . 15
|
122 | 121 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
↾t ↾t |
123 | 122 | rspcev 3309 |
. . . . . . . . . . . . 13
↾t
↾t |
124 | 102, 120,
123 | syl2anc 693 |
. . . . . . . . . . . 12
↾t
↾t |
125 | 124 | 3exp 1264 |
. . . . . . . . . . 11
↾t
↾t |
126 | 74, 125 | sylbi 207 |
. . . . . . . . . 10
↾t
↾t |
127 | 126 | rexlimiv 3027 |
. . . . . . . . 9
↾t
↾t |
128 | 73, 127 | syl6 35 |
. . . . . . . 8
↾t
↾t |
129 | 128 | com3r 87 |
. . . . . . 7
↾t
↾t |
130 | 72, 129 | mpd 15 |
. . . . . 6
↾t
↾t |
131 | 130 | ex 450 |
. . . . 5
↾t
↾t |
132 | 19, 131 | sylbird 250 |
. . . 4
↾t ↾t
↾t |
133 | 132 | com23 86 |
. . 3
↾t
↾t ↾t |
134 | 15, 133 | syld 47 |
. 2
↾t
↾t ↾t |
135 | 134 | ralrimdva 2969 |
1
↾t ↾t ↾t |