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	⊢ 𝐴 ∈ Sℋ
	cdj3lem2.2	⊢ 𝐵 ∈ Sℋ
	cdj3lem3.3	⊢ 𝑇 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
Assertion	cdj3lem3a	⊢ ( ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑇 ‘ 𝐶 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cdj3lem2.1	⊢ 𝐴 ∈ Sℋ
2		cdj3lem2.2	⊢ 𝐵 ∈ Sℋ
3		cdj3lem3.3	⊢ 𝑇 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
4	1 2	shseli	⊢ ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝐶 = ( 𝑣 +ℎ 𝑢 ) )
5	1 2 3	cdj3lem3	⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑇 ‘ ( 𝑣 +ℎ 𝑢 ) ) = 𝑢 )
6		simp2	⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → 𝑢 ∈ 𝐵 )
7	5 6	eqeltrd	⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑇 ‘ ( 𝑣 +ℎ 𝑢 ) ) ∈ 𝐵 )
8	7	3expa	⊢ ( ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑇 ‘ ( 𝑣 +ℎ 𝑢 ) ) ∈ 𝐵 )
9		fveq2	⊢ ( 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( 𝑇 ‘ 𝐶 ) = ( 𝑇 ‘ ( 𝑣 +ℎ 𝑢 ) ) )
10	9	eleq1d	⊢ ( 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( ( 𝑇 ‘ 𝐶 ) ∈ 𝐵 ↔ ( 𝑇 ‘ ( 𝑣 +ℎ 𝑢 ) ) ∈ 𝐵 ) )
11	8 10	syl5ibr	⊢ ( 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑇 ‘ 𝐶 ) ∈ 𝐵 ) )
12	11	expd	⊢ ( 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( 𝑇 ‘ 𝐶 ) ∈ 𝐵 ) ) )
13	12	com13	⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) → ( 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( 𝑇 ‘ 𝐶 ) ∈ 𝐵 ) ) )
14	13	rexlimdvv	⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( 𝑇 ‘ 𝐶 ) ∈ 𝐵 ) )
15	4 14	syl5bi	⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) → ( 𝑇 ‘ 𝐶 ) ∈ 𝐵 ) )
16	15	impcom	⊢ ( ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑇 ‘ 𝐶 ) ∈ 𝐵 )