Theorem updjudhf

Description: The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022)

	Ref	Expression
Hypotheses	updjud.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
	updjud.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐶 )
	updjudhf.h	⊢ 𝐻 = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) )
Assertion	updjudhf	⊢ ( 𝜑 → 𝐻 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		updjud.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
2		updjud.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐶 )
3		updjudhf.h	⊢ 𝐻 = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) )
4		eldju2ndl	⊢ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ∧ ( 1st ‘ 𝑥 ) = ∅ ) → ( 2nd ‘ 𝑥 ) ∈ 𝐴 )
5	4	ex	⊢ ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ( 1st ‘ 𝑥 ) = ∅ → ( 2nd ‘ 𝑥 ) ∈ 𝐴 ) )
6		ffvelrn	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) ∈ 𝐶 )
7	6	ex	⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 → ( ( 2nd ‘ 𝑥 ) ∈ 𝐴 → ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) ∈ 𝐶 ) )
8	1 7	syl	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑥 ) ∈ 𝐴 → ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) ∈ 𝐶 ) )
9	5 8	sylan9r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ) → ( ( 1st ‘ 𝑥 ) = ∅ → ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) ∈ 𝐶 ) )
10	9	imp	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ) ∧ ( 1st ‘ 𝑥 ) = ∅ ) → ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) ∈ 𝐶 )
11		df-ne	⊢ ( ( 1st ‘ 𝑥 ) ≠ ∅ ↔ ¬ ( 1st ‘ 𝑥 ) = ∅ )
12		eldju2ndr	⊢ ( ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ∧ ( 1st ‘ 𝑥 ) ≠ ∅ ) → ( 2nd ‘ 𝑥 ) ∈ 𝐵 )
13	12	ex	⊢ ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ( 1st ‘ 𝑥 ) ≠ ∅ → ( 2nd ‘ 𝑥 ) ∈ 𝐵 ) )
14		ffvelrn	⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ∈ 𝐶 )
15	14	ex	⊢ ( 𝐺 : 𝐵 ⟶ 𝐶 → ( ( 2nd ‘ 𝑥 ) ∈ 𝐵 → ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ∈ 𝐶 ) )
16	2 15	syl	⊢ ( 𝜑 → ( ( 2nd ‘ 𝑥 ) ∈ 𝐵 → ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ∈ 𝐶 ) )
17	13 16	sylan9r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ) → ( ( 1st ‘ 𝑥 ) ≠ ∅ → ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ∈ 𝐶 ) )
18	11 17	syl5bir	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ) → ( ¬ ( 1st ‘ 𝑥 ) = ∅ → ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ∈ 𝐶 ) )
19	18	imp	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ) ∧ ¬ ( 1st ‘ 𝑥 ) = ∅ ) → ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ∈ 𝐶 )
20	10 19	ifclda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ) → if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) ∈ 𝐶 )
21	20 3	fmptd	⊢ ( 𝜑 → 𝐻 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 )