Theorem cdj3lem3a

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

	Ref	Expression
Hypotheses	cdj3lem2.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
	cdj3lem2.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
	cdj3lem3.3	$$⊢T=\left(x\in \left(A{+}_{\mathscr{H}}B\right)⟼\left(\iota w\in B|\exists z\in Ax=z{+}_{ℎ}w\right)\right)$$
Assertion	cdj3lem3a	$$⊢\left(C\in \left(A{+}_{\mathscr{H}}B\right)\wedge A\cap B=0_{\mathscr{H}}\right)\to T\left(C\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		cdj3lem2.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		cdj3lem2.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3		cdj3lem3.3	$$⊢T=\left(x\in \left(A{+}_{\mathscr{H}}B\right)⟼\left(\iota w\in B|\exists z\in Ax=z{+}_{ℎ}w\right)\right)$$
4	1 2	shseli	$$⊢C\in \left(A{+}_{\mathscr{H}}B\right)\leftrightarrow \exists v\in A\exists u\in BC=v{+}_{ℎ}u$$
5	1 2 3	cdj3lem3	$$⊢\left(v\in A\wedge u\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to T\left(v{+}_{ℎ}u\right)=u$$
6		simp2	$$⊢\left(v\in A\wedge u\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to u\in B$$
7	5 6	eqeltrd	$$⊢\left(v\in A\wedge u\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to T\left(v{+}_{ℎ}u\right)\in B$$
8	7	3expa	$$⊢\left(\left(v\in A\wedge u\in B\right)\wedge A\cap B=0_{\mathscr{H}}\right)\to T\left(v{+}_{ℎ}u\right)\in B$$
9		fveq2	$$⊢C=v{+}_{ℎ}u\to T\left(C\right)=T\left(v{+}_{ℎ}u\right)$$
10	9	eleq1d	$$⊢C=v{+}_{ℎ}u\to \left(T\left(C\right)\in B\leftrightarrow T\left(v{+}_{ℎ}u\right)\in B\right)$$
11	8 10	imbitrrid	$$⊢C=v{+}_{ℎ}u\to \left(\left(\left(v\in A\wedge u\in B\right)\wedge A\cap B=0_{\mathscr{H}}\right)\to T\left(C\right)\in B\right)$$
12	11	expd	$$⊢C=v{+}_{ℎ}u\to \left(\left(v\in A\wedge u\in B\right)\to \left(A\cap B=0_{\mathscr{H}}\to T\left(C\right)\in B\right)\right)$$
13	12	com13	$$⊢A\cap B=0_{\mathscr{H}}\to \left(\left(v\in A\wedge u\in B\right)\to \left(C=v{+}_{ℎ}u\to T\left(C\right)\in B\right)\right)$$
14	13	rexlimdvv	$$⊢A\cap B=0_{\mathscr{H}}\to \left(\exists v\in A\exists u\in BC=v{+}_{ℎ}u\to T\left(C\right)\in B\right)$$
15	4 14	biimtrid	$$⊢A\cap B=0_{\mathscr{H}}\to \left(C\in \left(A{+}_{\mathscr{H}}B\right)\to T\left(C\right)\in B\right)$$
16	15	impcom	$$⊢\left(C\in \left(A{+}_{\mathscr{H}}B\right)\wedge A\cap B=0_{\mathscr{H}}\right)\to T\left(C\right)\in B$$