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

Proof

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