# Metamath Proof Explorer

## 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}\in {\mathbf{S}}_{ℋ}$
cdj3lem2.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
cdj3lem2.3 ${⊢}{S}=\left({x}\in \left({A}{+}_{ℋ}{B}\right)⟼\left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{w}\right)\right)$
Assertion cdj3lem2a ${⊢}\left({C}\in \left({A}{+}_{ℋ}{B}\right)\wedge {A}\cap {B}={0}_{ℋ}\right)\to {S}\left({C}\right)\in {A}$

### Proof

Step Hyp Ref Expression
1 cdj3lem2.1 ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
2 cdj3lem2.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
3 cdj3lem2.3 ${⊢}{S}=\left({x}\in \left({A}{+}_{ℋ}{B}\right)⟼\left(\iota {z}\in {A}|\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{w}\right)\right)$
4 1 2 shseli ${⊢}{C}\in \left({A}{+}_{ℋ}{B}\right)↔\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}\exists {u}\in {B}\phantom{\rule{.4em}{0ex}}{C}={v}{+}_{ℎ}{u}$
5 1 2 3 cdj3lem2 ${⊢}\left({v}\in {A}\wedge {u}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {S}\left({v}{+}_{ℎ}{u}\right)={v}$
6 simp1 ${⊢}\left({v}\in {A}\wedge {u}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {v}\in {A}$
7 5 6 eqeltrd ${⊢}\left({v}\in {A}\wedge {u}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {S}\left({v}{+}_{ℎ}{u}\right)\in {A}$
8 7 3expa ${⊢}\left(\left({v}\in {A}\wedge {u}\in {B}\right)\wedge {A}\cap {B}={0}_{ℋ}\right)\to {S}\left({v}{+}_{ℎ}{u}\right)\in {A}$
9 fveq2 ${⊢}{C}={v}{+}_{ℎ}{u}\to {S}\left({C}\right)={S}\left({v}{+}_{ℎ}{u}\right)$
10 9 eleq1d ${⊢}{C}={v}{+}_{ℎ}{u}\to \left({S}\left({C}\right)\in {A}↔{S}\left({v}{+}_{ℎ}{u}\right)\in {A}\right)$
11 8 10 syl5ibr ${⊢}{C}={v}{+}_{ℎ}{u}\to \left(\left(\left({v}\in {A}\wedge {u}\in {B}\right)\wedge {A}\cap {B}={0}_{ℋ}\right)\to {S}\left({C}\right)\in {A}\right)$
12 11 expd ${⊢}{C}={v}{+}_{ℎ}{u}\to \left(\left({v}\in {A}\wedge {u}\in {B}\right)\to \left({A}\cap {B}={0}_{ℋ}\to {S}\left({C}\right)\in {A}\right)\right)$
13 12 com13 ${⊢}{A}\cap {B}={0}_{ℋ}\to \left(\left({v}\in {A}\wedge {u}\in {B}\right)\to \left({C}={v}{+}_{ℎ}{u}\to {S}\left({C}\right)\in {A}\right)\right)$
14 13 rexlimdvv ${⊢}{A}\cap {B}={0}_{ℋ}\to \left(\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}\exists {u}\in {B}\phantom{\rule{.4em}{0ex}}{C}={v}{+}_{ℎ}{u}\to {S}\left({C}\right)\in {A}\right)$
15 4 14 syl5bi ${⊢}{A}\cap {B}={0}_{ℋ}\to \left({C}\in \left({A}{+}_{ℋ}{B}\right)\to {S}\left({C}\right)\in {A}\right)$
16 15 impcom ${⊢}\left({C}\in \left({A}{+}_{ℋ}{B}\right)\wedge {A}\cap {B}={0}_{ℋ}\right)\to {S}\left({C}\right)\in {A}$