Metamath Proof Explorer

Theorem 3oalem3

Description: Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	3oalem1.1	$⊢ B \in C_{ℋ}$
		3oalem1.2	$⊢ C \in C_{ℋ}$
		3oalem1.3	$⊢ R \in C_{ℋ}$
		3oalem1.4	$⊢ S \in C_{ℋ}$
	Assertion	3oalem3	$⊢ (B +_{ℋ} R) \cap (C +_{ℋ} S) \subseteq B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S))))$

Proof

Step	Hyp	Ref	Expression
1		3oalem1.1	$⊢ B \in C_{ℋ}$
2		3oalem1.2	$⊢ C \in C_{ℋ}$
3		3oalem1.3	$⊢ R \in C_{ℋ}$
4		3oalem1.4	$⊢ S \in C_{ℋ}$
5	1 3	chseli	$⊢ v \in (B +_{ℋ} R) \leftrightarrow \exists x \in B \exists y \in R v = x +_{ℎ} y$
6		r2ex	$⊢ \exists x \in B \exists y \in R v = x +_{ℎ} y \leftrightarrow \exists x \exists y ((x \in B \land y \in R) \land v = x +_{ℎ} y)$
7	5 6	bitri	$⊢ v \in (B +_{ℋ} R) \leftrightarrow \exists x \exists y ((x \in B \land y \in R) \land v = x +_{ℎ} y)$
8	2 4	chseli	$⊢ v \in (C +_{ℋ} S) \leftrightarrow \exists z \in C \exists w \in S v = z +_{ℎ} w$
9		r2ex	$⊢ \exists z \in C \exists w \in S v = z +_{ℎ} w \leftrightarrow \exists z \exists w ((z \in C \land w \in S) \land v = z +_{ℎ} w)$
10	8 9	bitri	$⊢ v \in (C +_{ℋ} S) \leftrightarrow \exists z \exists w ((z \in C \land w \in S) \land v = z +_{ℎ} w)$
11	7 10	anbi12i	$⊢ (v \in (B +_{ℋ} R) \land v \in (C +_{ℋ} S)) \leftrightarrow (\exists x \exists y ((x \in B \land y \in R) \land v = x +_{ℎ} y) \land \exists z \exists w ((z \in C \land w \in S) \land v = z +_{ℎ} w))$
12		elin	$⊢ v \in ((B +_{ℋ} R) \cap (C +_{ℋ} S)) \leftrightarrow (v \in (B +_{ℋ} R) \land v \in (C +_{ℋ} S))$
13		4exdistrv	$⊢ \exists x \exists z \exists y \exists w (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \leftrightarrow (\exists x \exists y ((x \in B \land y \in R) \land v = x +_{ℎ} y) \land \exists z \exists w ((z \in C \land w \in S) \land v = z +_{ℎ} w))$
14	11 12 13	3bitr4i	$⊢ v \in ((B +_{ℋ} R) \cap (C +_{ℋ} S)) \leftrightarrow \exists x \exists z \exists y \exists w (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w))$
15	1 2 3 4	3oalem2	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to v \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)))))$
16	15	exlimivv	$⊢ \exists y \exists w (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to v \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)))))$
17	16	exlimivv	$⊢ \exists x \exists z \exists y \exists w (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to v \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)))))$
18	14 17	sylbi	$⊢ v \in ((B +_{ℋ} R) \cap (C +_{ℋ} S)) \to v \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)))))$
19	18	ssriv	$⊢ (B +_{ℋ} R) \cap (C +_{ℋ} S) \subseteq B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S))))$