# Metamath Proof Explorer

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

### Proof

Step Hyp Ref Expression
1 cdj3lem2.1 ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
2 cdj3lem2.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
3 cdj3lem3.3 ${⊢}{T}=\left({x}\in \left({A}{+}_{ℋ}{B}\right)⟼\left(\iota {w}\in {B}|\exists {z}\in {A}\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 cdj3lem3 ${⊢}\left({v}\in {A}\wedge {u}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {T}\left({v}{+}_{ℎ}{u}\right)={u}$
6 simp2 ${⊢}\left({v}\in {A}\wedge {u}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {u}\in {B}$
7 5 6 eqeltrd ${⊢}\left({v}\in {A}\wedge {u}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\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}_{ℋ}\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}↔{T}\left({v}{+}_{ℎ}{u}\right)\in {B}\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 {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}_{ℋ}\to {T}\left({C}\right)\in {B}\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 {T}\left({C}\right)\in {B}\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 {T}\left({C}\right)\in {B}\right)$
15 4 14 syl5bi ${⊢}{A}\cap {B}={0}_{ℋ}\to \left({C}\in \left({A}{+}_{ℋ}{B}\right)\to {T}\left({C}\right)\in {B}\right)$
16 15 impcom ${⊢}\left({C}\in \left({A}{+}_{ℋ}{B}\right)\wedge {A}\cap {B}={0}_{ℋ}\right)\to {T}\left({C}\right)\in {B}$