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 = Atoms K
padd0.p + ˙ = + 𝑃 K
Assertion elpadd0 K B X A Y A ¬ X Y S X + ˙ Y S X S Y

Proof

Step Hyp Ref Expression
1 padd0.a A = Atoms K
2 padd0.p + ˙ = + 𝑃 K
3 neanior X Y ¬ X = Y =
4 3 bicomi ¬ X = Y = X Y
5 4 con1bii ¬ X Y X = Y =
6 eqid K = K
7 eqid join K = join K
8 6 7 1 2 elpadd K B X A Y A S X + ˙ Y S X S Y S A q X r Y S K q join K r
9 rex0 ¬ q r Y S K q join K r
10 rexeq X = q X r Y S K q join K r q r Y S K q join K r
11 9 10 mtbiri X = ¬ q X r Y S K q join K r
12 rex0 ¬ r S K q join K r
13 12 a1i q X ¬ r S K q join K r
14 13 nrex ¬ q X r S K q join K r
15 rexeq Y = r Y S K q join K r r S K q join K r
16 15 rexbidv Y = q X r Y S K q join K r q X r S K q join K r
17 14 16 mtbiri Y = ¬ q X r Y S K q join K r
18 11 17 jaoi X = Y = ¬ q X r Y S K q join K r
19 18 intnand X = Y = ¬ S A q X r Y S K q join K r
20 biorf ¬ S A q X r Y S K q join K r S X S Y S A q X r Y S K q join K r S X S Y
21 19 20 syl X = Y = S X S Y S A q X r Y S K q join K r S X S Y
22 orcom S A q X r Y S K q join K r S X S Y S X S Y S A q X r Y S K q join K r
23 21 22 bitr2di X = Y = S X S Y S A q X r Y S K q join K r S X S Y
24 8 23 sylan9bb K B X A Y A X = Y = S X + ˙ Y S X S Y
25 5 24 sylan2b K B X A Y A ¬ X Y S X + ˙ Y S X S Y