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 e. SH
	cdj3lem2.2	|- B e. SH
	cdj3lem3.3	|- T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )
Assertion	cdj3lem3a	|- ( ( C e. ( A +H B ) /\ ( A i^i B ) = 0H ) -> ( T ` C ) e. B )

Proof

Step	Hyp	Ref	Expression
1		cdj3lem2.1	|- A e. SH
2		cdj3lem2.2	|- B e. SH
3		cdj3lem3.3	|- T = ( x e. ( A +H B ) |-> ( iota_ w e. B E. z e. A x = ( z +h w ) ) )
4	1 2	shseli	|- ( C e. ( A +H B ) <-> E. v e. A E. u e. B C = ( v +h u ) )
5	1 2 3	cdj3lem3	|- ( ( v e. A /\ u e. B /\ ( A i^i B ) = 0H ) -> ( T ` ( v +h u ) ) = u )
6		simp2	|- ( ( v e. A /\ u e. B /\ ( A i^i B ) = 0H ) -> u e. B )
7	5 6	eqeltrd	|- ( ( v e. A /\ u e. B /\ ( A i^i B ) = 0H ) -> ( T ` ( v +h u ) ) e. B )
8	7	3expa	|- ( ( ( v e. A /\ u e. B ) /\ ( A i^i B ) = 0H ) -> ( T ` ( v +h u ) ) e. B )
9		fveq2	|- ( C = ( v +h u ) -> ( T ` C ) = ( T ` ( v +h u ) ) )
10	9	eleq1d	|- ( C = ( v +h u ) -> ( ( T ` C ) e. B <-> ( T ` ( v +h u ) ) e. B ) )
11	8 10	syl5ibr	|- ( C = ( v +h u ) -> ( ( ( v e. A /\ u e. B ) /\ ( A i^i B ) = 0H ) -> ( T ` C ) e. B ) )
12	11	expd	|- ( C = ( v +h u ) -> ( ( v e. A /\ u e. B ) -> ( ( A i^i B ) = 0H -> ( T ` C ) e. B ) ) )
13	12	com13	|- ( ( A i^i B ) = 0H -> ( ( v e. A /\ u e. B ) -> ( C = ( v +h u ) -> ( T ` C ) e. B ) ) )
14	13	rexlimdvv	|- ( ( A i^i B ) = 0H -> ( E. v e. A E. u e. B C = ( v +h u ) -> ( T ` C ) e. B ) )
15	4 14	syl5bi	|- ( ( A i^i B ) = 0H -> ( C e. ( A +H B ) -> ( T ` C ) e. B ) )
16	15	impcom	|- ( ( C e. ( A +H B ) /\ ( A i^i B ) = 0H ) -> ( T ` C ) e. B )