Description: A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fissuni | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | dfss3 | |
|
3 | eluni2 | |
|
4 | 3 | ralbii | |
5 | 2 4 | sylbb | |
6 | 5 | adantr | |
7 | eleq2 | |
|
8 | 7 | ac6sfi | |
9 | 1 6 8 | syl2anc | |
10 | fimass | |
|
11 | vex | |
|
12 | 11 | imaex | |
13 | 12 | elpw | |
14 | 10 13 | sylibr | |
15 | 14 | ad2antrl | |
16 | ffun | |
|
17 | 16 | ad2antrl | |
18 | simplr | |
|
19 | imafi | |
|
20 | 17 18 19 | syl2anc | |
21 | 15 20 | elind | |
22 | ffn | |
|
23 | 22 | adantr | |
24 | ssidd | |
|
25 | simpr | |
|
26 | fnfvima | |
|
27 | 23 24 25 26 | syl3anc | |
28 | elssuni | |
|
29 | 27 28 | syl | |
30 | 29 | sseld | |
31 | 30 | ralimdva | |
32 | 31 | imp | |
33 | dfss3 | |
|
34 | 32 33 | sylibr | |
35 | 34 | adantl | |
36 | unieq | |
|
37 | 36 | sseq2d | |
38 | 37 | rspcev | |
39 | 21 35 38 | syl2anc | |
40 | 9 39 | exlimddv | |