Description: Two ways of expressing the statement "there is a cover of A by elements of B such that for each set in the cover, ph ". Note that ph and x must be distinct. (Contributed by Jeff Madsen, 20-Jun-2010)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cover2.1 | |
|
cover2.2 | |
||
Assertion | cover2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cover2.1 | |
|
2 | cover2.2 | |
|
3 | ssrab2 | |
|
4 | 1 3 | elpwi2 | |
5 | nfra1 | |
|
6 | 3 | unissi | |
7 | 6 | sseli | |
8 | 7 2 | eleqtrrdi | |
9 | rsp | |
|
10 | elunirab | |
|
11 | 9 10 | syl6ibr | |
12 | 8 11 | impbid2 | |
13 | 5 12 | alrimi | |
14 | dfcleq | |
|
15 | 13 14 | sylibr | |
16 | nfrab1 | |
|
17 | 16 | nfeq2 | |
18 | eleq2 | |
|
19 | rabid | |
|
20 | 19 | simprbi | |
21 | 18 20 | syl6bi | |
22 | 17 21 | ralrimi | |
23 | unieq | |
|
24 | 23 | eqeq1d | |
25 | 24 | anbi1d | |
26 | 22 25 | mpbiran2d | |
27 | 26 | rspcev | |
28 | 4 15 27 | sylancr | |
29 | elpwi | |
|
30 | r19.29r | |
|
31 | 30 | expcom | |
32 | ssrexv | |
|
33 | 31 32 | sylan9r | |
34 | 29 33 | sylan | |
35 | eleq2 | |
|
36 | 35 | biimpar | |
37 | eluni2 | |
|
38 | 36 37 | sylib | |
39 | 34 38 | impel | |
40 | 39 | anassrs | |
41 | 40 | ralrimiva | |
42 | 41 | anasss | |
43 | 42 | ancom2s | |
44 | 43 | rexlimiva | |
45 | 28 44 | impbii | |