Theorem updjudhcoinrg

Description: The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second function. (Contributed by AV, 27-Jun-2022)

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

Proof

Step	Hyp	Ref	Expression
1		updjud.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
2		updjud.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐶 )
3		updjudhf.h	⊢ 𝐻 = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) )
4	1 2 3	updjudhf	⊢ ( 𝜑 → 𝐻 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 )
5	4	ffnd	⊢ ( 𝜑 → 𝐻 Fn ( 𝐴 ⊔ 𝐵 ) )
6		inrresf	⊢ ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 )
7		ffn	⊢ ( ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 ) → ( inr ↾ 𝐵 ) Fn 𝐵 )
8	6 7	mp1i	⊢ ( 𝜑 → ( inr ↾ 𝐵 ) Fn 𝐵 )
9		frn	⊢ ( ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 ) → ran ( inr ↾ 𝐵 ) ⊆ ( 𝐴 ⊔ 𝐵 ) )
10	6 9	mp1i	⊢ ( 𝜑 → ran ( inr ↾ 𝐵 ) ⊆ ( 𝐴 ⊔ 𝐵 ) )
11		fnco	⊢ ( ( 𝐻 Fn ( 𝐴 ⊔ 𝐵 ) ∧ ( inr ↾ 𝐵 ) Fn 𝐵 ∧ ran ( inr ↾ 𝐵 ) ⊆ ( 𝐴 ⊔ 𝐵 ) ) → ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) Fn 𝐵 )
12	5 8 10 11	syl3anc	⊢ ( 𝜑 → ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) Fn 𝐵 )
13	2	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
14		fvco2	⊢ ( ( ( inr ↾ 𝐵 ) Fn 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑏 ) = ( 𝐻 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) ) )
15	8 14	sylan	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑏 ) = ( 𝐻 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) ) )
16		fvres	⊢ ( 𝑏 ∈ 𝐵 → ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) = ( inr ‘ 𝑏 ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) = ( inr ‘ 𝑏 ) )
18	17	fveq2d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐻 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝐻 ‘ ( inr ‘ 𝑏 ) ) )
19		fveqeq2	⊢ ( 𝑥 = ( inr ‘ 𝑏 ) → ( ( 1st ‘ 𝑥 ) = ∅ ↔ ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ ) )
20		2fveq3	⊢ ( 𝑥 = ( inr ‘ 𝑏 ) → ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
21		2fveq3	⊢ ( 𝑥 = ( inr ‘ 𝑏 ) → ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
22	19 20 21	ifbieq12d	⊢ ( 𝑥 = ( inr ‘ 𝑏 ) → if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) = if ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) , ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) ) )
23	22	adantl	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑥 = ( inr ‘ 𝑏 ) ) → if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) = if ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) , ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) ) )
24		1stinr	⊢ ( 𝑏 ∈ 𝐵 → ( 1st ‘ ( inr ‘ 𝑏 ) ) = 1o )
25		1n0	⊢ 1o ≠ ∅
26	25	neii	⊢ ¬ 1o = ∅
27		eqeq1	⊢ ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = 1o → ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ ↔ 1o = ∅ ) )
28	26 27	mtbiri	⊢ ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = 1o → ¬ ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ )
29	24 28	syl	⊢ ( 𝑏 ∈ 𝐵 → ¬ ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ )
30	29	adantl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ¬ ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ )
31	30	adantr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑥 = ( inr ‘ 𝑏 ) ) → ¬ ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ )
32	31	iffalsed	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑥 = ( inr ‘ 𝑏 ) ) → if ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) , ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) ) = ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
33	23 32	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑥 = ( inr ‘ 𝑏 ) ) → if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) = ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
34		djurcl	⊢ ( 𝑏 ∈ 𝐵 → ( inr ‘ 𝑏 ) ∈ ( 𝐴 ⊔ 𝐵 ) )
35	34	adantl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( inr ‘ 𝑏 ) ∈ ( 𝐴 ⊔ 𝐵 ) )
36	2	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐺 : 𝐵 ⟶ 𝐶 )
37		2ndinr	⊢ ( 𝑏 ∈ 𝐵 → ( 2nd ‘ ( inr ‘ 𝑏 ) ) = 𝑏 )
38	37	adantl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 2nd ‘ ( inr ‘ 𝑏 ) ) = 𝑏 )
39		simpr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
40	38 39	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 2nd ‘ ( inr ‘ 𝑏 ) ) ∈ 𝐵 )
41	36 40	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) ∈ 𝐶 )
42	3 33 35 41	fvmptd2	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐻 ‘ ( inr ‘ 𝑏 ) ) = ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
43	18 42	eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐻 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
44	38	fveq2d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) = ( 𝐺 ‘ 𝑏 ) )
45	15 43 44	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) )
46	12 13 45	eqfnfvd	⊢ ( 𝜑 → ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 )