Theorem updjudhcoinlf 9844

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

Hypotheses

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

Assertion

Ref	Expression
updjudhcoinlf	⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) = 𝐹)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝜑,𝑥   𝑥,𝐹

Allowed substitution hints:   𝐺(𝑥)   𝐻(𝑥)

Proof of Theorem updjudhcoinlf

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		updjud.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
2		updjud.g	. . . . 5 ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)
3		updjudhf.h	. . . . 5 ⊢ 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))))
4	1, 2, 3	updjudhf 9843	. . . 4 ⊢ (𝜑 → 𝐻:(𝐴 ⊔ 𝐵)⟶𝐶)
5	4	ffnd 6663	. . 3 ⊢ (𝜑 → 𝐻 Fn (𝐴 ⊔ 𝐵))
6		inlresf 9826	. . . 4 ⊢ (inl ↾ 𝐴):𝐴⟶(𝐴 ⊔ 𝐵)
7		ffn 6662	. . . 4 ⊢ ((inl ↾ 𝐴):𝐴⟶(𝐴 ⊔ 𝐵) → (inl ↾ 𝐴) Fn 𝐴)
8	6, 7	mp1i 13	. . 3 ⊢ (𝜑 → (inl ↾ 𝐴) Fn 𝐴)
9		frn 6669	. . . 4 ⊢ ((inl ↾ 𝐴):𝐴⟶(𝐴 ⊔ 𝐵) → ran (inl ↾ 𝐴) ⊆ (𝐴 ⊔ 𝐵))
10	6, 9	mp1i 13	. . 3 ⊢ (𝜑 → ran (inl ↾ 𝐴) ⊆ (𝐴 ⊔ 𝐵))
11		fnco 6610	. . 3 ⊢ ((𝐻 Fn (𝐴 ⊔ 𝐵) ∧ (inl ↾ 𝐴) Fn 𝐴 ∧ ran (inl ↾ 𝐴) ⊆ (𝐴 ⊔ 𝐵)) → (𝐻 ∘ (inl ↾ 𝐴)) Fn 𝐴)
12	5, 8, 10, 11	syl3anc 1373	. 2 ⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) Fn 𝐴)
13	1	ffnd 6663	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
14		fvco2 6931	. . . 4 ⊢ (((inl ↾ 𝐴) Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → ((𝐻 ∘ (inl ↾ 𝐴))‘𝑎) = (𝐻‘((inl ↾ 𝐴)‘𝑎)))
15	8, 14	sylan 580	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐻 ∘ (inl ↾ 𝐴))‘𝑎) = (𝐻‘((inl ↾ 𝐴)‘𝑎)))
16		fvres 6853	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → ((inl ↾ 𝐴)‘𝑎) = (inl‘𝑎))
17	16	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((inl ↾ 𝐴)‘𝑎) = (inl‘𝑎))
18	17	fveq2d 6838	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐻‘((inl ↾ 𝐴)‘𝑎)) = (𝐻‘(inl‘𝑎)))
19		fveqeq2 6843	. . . . . . . 8 ⊢ (𝑥 = (inl‘𝑎) → ((1st ‘𝑥) = ∅ ↔ (1st ‘(inl‘𝑎)) = ∅))
20		2fveq3 6839	. . . . . . . 8 ⊢ (𝑥 = (inl‘𝑎) → (𝐹‘(2nd ‘𝑥)) = (𝐹‘(2nd ‘(inl‘𝑎))))
21		2fveq3 6839	. . . . . . . 8 ⊢ (𝑥 = (inl‘𝑎) → (𝐺‘(2nd ‘𝑥)) = (𝐺‘(2nd ‘(inl‘𝑎))))
22	19, 20, 21	ifbieq12d 4508	. . . . . . 7 ⊢ (𝑥 = (inl‘𝑎) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = if((1st ‘(inl‘𝑎)) = ∅, (𝐹‘(2nd ‘(inl‘𝑎))), (𝐺‘(2nd ‘(inl‘𝑎)))))
23	22	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = if((1st ‘(inl‘𝑎)) = ∅, (𝐹‘(2nd ‘(inl‘𝑎))), (𝐺‘(2nd ‘(inl‘𝑎)))))
24		1stinl 9839	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐴 → (1st ‘(inl‘𝑎)) = ∅)
25	24	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (1st ‘(inl‘𝑎)) = ∅)
26	25	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → (1st ‘(inl‘𝑎)) = ∅)
27	26	iftrued 4487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → if((1st ‘(inl‘𝑎)) = ∅, (𝐹‘(2nd ‘(inl‘𝑎))), (𝐺‘(2nd ‘(inl‘𝑎)))) = (𝐹‘(2nd ‘(inl‘𝑎))))
28	23, 27	eqtrd 2771	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = (𝐹‘(2nd ‘(inl‘𝑎))))
29		djulcl 9822	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → (inl‘𝑎) ∈ (𝐴 ⊔ 𝐵))
30	29	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (inl‘𝑎) ∈ (𝐴 ⊔ 𝐵))
31	1	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐹:𝐴⟶𝐶)
32		2ndinl 9840	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → (2nd ‘(inl‘𝑎)) = 𝑎)
33	32	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (2nd ‘(inl‘𝑎)) = 𝑎)
34		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴)
35	33, 34	eqeltrd 2836	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (2nd ‘(inl‘𝑎)) ∈ 𝐴)
36	31, 35	ffvelcdmd 7030	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘(2nd ‘(inl‘𝑎))) ∈ 𝐶)
37	3, 28, 30, 36	fvmptd2 6949	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐻‘(inl‘𝑎)) = (𝐹‘(2nd ‘(inl‘𝑎))))
38	18, 37	eqtrd 2771	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐻‘((inl ↾ 𝐴)‘𝑎)) = (𝐹‘(2nd ‘(inl‘𝑎))))
39	33	fveq2d 6838	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘(2nd ‘(inl‘𝑎))) = (𝐹‘𝑎))
40	15, 38, 39	3eqtrd 2775	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐻 ∘ (inl ↾ 𝐴))‘𝑎) = (𝐹‘𝑎))
41	12, 13, 40	eqfnfvd 6979	1 ⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ⊆ wss 3901  ∅c0 4285  ifcif 4479   ↦ cmpt 5179  ran crn 5625   ↾ cres 5626   ∘ ccom 5628   Fn wfn 6487  ⟶wf 6488  ‘cfv 6492  1^st c1st 7931  2^nd c2nd 7932   ⊔ cdju 9810  inlcinl 9811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-1st 7933  df-2nd 7934  df-1o 8397  df-dju 9813  df-inl 9814

This theorem is referenced by:  updjud  9846