Metamath Proof Explorer


Theorem elpadd0

Description: Member of projective subspace sum with at least one empty set. (Contributed by NM, 29-Dec-2011)

Ref Expression
Hypotheses padd0.a A=AtomsK
padd0.p +˙=+𝑃K
Assertion elpadd0 KBXAYA¬XYSX+˙YSXSY

Proof

Step Hyp Ref Expression
1 padd0.a A=AtomsK
2 padd0.p +˙=+𝑃K
3 neanior XY¬X=Y=
4 3 bicomi ¬X=Y=XY
5 4 con1bii ¬XYX=Y=
6 eqid K=K
7 eqid joinK=joinK
8 6 7 1 2 elpadd KBXAYASX+˙YSXSYSAqXrYSKqjoinKr
9 rex0 ¬qrYSKqjoinKr
10 rexeq X=qXrYSKqjoinKrqrYSKqjoinKr
11 9 10 mtbiri X=¬qXrYSKqjoinKr
12 rex0 ¬rSKqjoinKr
13 12 a1i qX¬rSKqjoinKr
14 13 nrex ¬qXrSKqjoinKr
15 rexeq Y=rYSKqjoinKrrSKqjoinKr
16 15 rexbidv Y=qXrYSKqjoinKrqXrSKqjoinKr
17 14 16 mtbiri Y=¬qXrYSKqjoinKr
18 11 17 jaoi X=Y=¬qXrYSKqjoinKr
19 18 intnand X=Y=¬SAqXrYSKqjoinKr
20 biorf ¬SAqXrYSKqjoinKrSXSYSAqXrYSKqjoinKrSXSY
21 19 20 syl X=Y=SXSYSAqXrYSKqjoinKrSXSY
22 orcom SAqXrYSKqjoinKrSXSYSXSYSAqXrYSKqjoinKr
23 21 22 bitr2di X=Y=SXSYSAqXrYSKqjoinKrSXSY
24 8 23 sylan9bb KBXAYAX=Y=SX+˙YSXSY
25 5 24 sylan2b KBXAYA¬XYSX+˙YSXSY