Metamath Proof Explorer


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 ↾ 𝐵 ) ) = 𝐺 )