cdj3lem2a

Description: Lemma for cdj3i . Closure of the first-component function S . (Contributed by NM, 25-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdj3lem2.1	$⊢ A \in S_{ℋ}$
	cdj3lem2.2	$⊢ B \in S_{ℋ}$
	cdj3lem2.3	$⊢ S = (x \in (A +_{ℋ} B) ⟼ (ι z \in A \| \exists w \in B x = z +_{ℎ} w))$
Assertion	cdj3lem2a	$⊢ (C \in (A +_{ℋ} B) \land A \cap B = 0_{ℋ}) \to S (C) \in A$

Step	Hyp	Ref	Expression
1		cdj3lem2.1	$⊢ A \in S_{ℋ}$
2		cdj3lem2.2	$⊢ B \in S_{ℋ}$
3		cdj3lem2.3	$⊢ S = (x \in (A +_{ℋ} B) ⟼ (ι z \in A \| \exists w \in B x = z +_{ℎ} w))$
4	1 2	shseli	$⊢ C \in (A +_{ℋ} B) \leftrightarrow \exists v \in A \exists u \in B C = v +_{ℎ} u$
5	1 2 3	cdj3lem2	$⊢ (v \in A \land u \in B \land A \cap B = 0_{ℋ}) \to S (v +_{ℎ} u) = v$
6		simp1	$⊢ (v \in A \land u \in B \land A \cap B = 0_{ℋ}) \to v \in A$
7	5 6	eqeltrd	$⊢ (v \in A \land u \in B \land A \cap B = 0_{ℋ}) \to S (v +_{ℎ} u) \in A$
8	7	3expa	$⊢ ((v \in A \land u \in B) \land A \cap B = 0_{ℋ}) \to S (v +_{ℎ} u) \in A$
9		fveq2	$⊢ C = v +_{ℎ} u \to S (C) = S (v +_{ℎ} u)$
10	9	eleq1d	$⊢ C = v +_{ℎ} u \to (S (C) \in A \leftrightarrow S (v +_{ℎ} u) \in A)$
11	8 10	imbitrrid	$⊢ C = v +_{ℎ} u \to (((v \in A \land u \in B) \land A \cap B = 0_{ℋ}) \to S (C) \in A)$
12	11	expd	$⊢ C = v +_{ℎ} u \to ((v \in A \land u \in B) \to (A \cap B = 0_{ℋ} \to S (C) \in A))$
13	12	com13	$⊢ A \cap B = 0_{ℋ} \to ((v \in A \land u \in B) \to (C = v +_{ℎ} u \to S (C) \in A))$
14	13	rexlimdvv	$⊢ A \cap B = 0_{ℋ} \to (\exists v \in A \exists u \in B C = v +_{ℎ} u \to S (C) \in A)$
15	4 14	biimtrid	$⊢ A \cap B = 0_{ℋ} \to (C \in (A +_{ℋ} B) \to S (C) \in A)$
16	15	impcom	$⊢ (C \in (A +_{ℋ} B) \land A \cap B = 0_{ℋ}) \to S (C) \in A$

Metamath Proof Explorer