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 ∈ S ℋ
cdj3lem2.2 ⊢ B ∈ S ℋ
cdj3lem3.3 ⊢ T = x ∈ A + ℋ B ⟼ ι w ∈ B | ∃ z ∈ A x = z + ℎ w
Assertion cdj3lem3a ⊢ C ∈ A + ℋ B ∧ A ∩ B = 0 ℋ → T ⁡ C ∈ B

Proof

Step Hyp Ref Expression
1 cdj3lem2.1 ⊢ A ∈ S ℋ
2 cdj3lem2.2 ⊢ B ∈ S ℋ
3 cdj3lem3.3 ⊢ T = x ∈ A + ℋ B ⟼ ι w ∈ B | ∃ z ∈ A x = z + ℎ w
4 1 2 shseli ⊢ C ∈ A + ℋ B ↔ ∃ v ∈ A ∃ u ∈ B C = v + ℎ u
5 1 2 3 cdj3lem3 ⊢ v ∈ A ∧ u ∈ B ∧ A ∩ B = 0 ℋ → T ⁡ v + ℎ u = u
6 simp2 ⊢ v ∈ A ∧ u ∈ B ∧ A ∩ B = 0 ℋ → u ∈ B
7 5 6 eqeltrd ⊢ v ∈ A ∧ u ∈ B ∧ A ∩ B = 0 ℋ → T ⁡ v + ℎ u ∈ B
8 7 3expa ⊢ v ∈ A ∧ u ∈ B ∧ A ∩ B = 0 ℋ → T ⁡ v + ℎ u ∈ B
9 fveq2 ⊢ C = v + ℎ u → T ⁡ C = T ⁡ v + ℎ u
10 9 eleq1d ⊢ C = v + ℎ u → T ⁡ C ∈ B ↔ T ⁡ v + ℎ u ∈ B
11 8 10 imbitrrid ⊢ C = v + ℎ u → v ∈ A ∧ u ∈ B ∧ A ∩ B = 0 ℋ → T ⁡ C ∈ B
12 11 expd ⊢ C = v + ℎ u → v ∈ A ∧ u ∈ B → A ∩ B = 0 ℋ → T ⁡ C ∈ B
13 12 com13 ⊢ A ∩ B = 0 ℋ → v ∈ A ∧ u ∈ B → C = v + ℎ u → T ⁡ C ∈ B
14 13 rexlimdvv ⊢ A ∩ B = 0 ℋ → ∃ v ∈ A ∃ u ∈ B C = v + ℎ u → T ⁡ C ∈ B
15 4 14 biimtrid ⊢ A ∩ B = 0 ℋ → C ∈ A + ℋ B → T ⁡ C ∈ B
16 15 impcom ⊢ C ∈ A + ℋ B ∧ A ∩ B = 0 ℋ → T ⁡ C ∈ B