Description: Member of projective subspace sum with at least one empty set. (Contributed by NM, 29-Dec-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | padd0.a | |
|
padd0.p | |
||
Assertion | elpadd0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | padd0.a | |
|
2 | padd0.p | |
|
3 | neanior | |
|
4 | 3 | bicomi | |
5 | 4 | con1bii | |
6 | eqid | |
|
7 | eqid | |
|
8 | 6 7 1 2 | elpadd | |
9 | rex0 | |
|
10 | rexeq | |
|
11 | 9 10 | mtbiri | |
12 | rex0 | |
|
13 | 12 | a1i | |
14 | 13 | nrex | |
15 | rexeq | |
|
16 | 15 | rexbidv | |
17 | 14 16 | mtbiri | |
18 | 11 17 | jaoi | |
19 | 18 | intnand | |
20 | biorf | |
|
21 | 19 20 | syl | |
22 | orcom | |
|
23 | 21 22 | bitr2di | |
24 | 8 23 | sylan9bb | |
25 | 5 24 | sylan2b | |