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	$⊢ φ \to F : A ⟶ C$
	updjud.g	$⊢ φ \to G : B ⟶ C$
	updjudhf.h	$⊢ H = (x \in (A ⊔︀ B) ⟼ if (1^{st} (x) = \emptyset, F (2^{nd} (x)), G (2^{nd} (x))))$
Assertion	updjudhcoinrg	$⊢ φ \to H \circ ({inr ↾}_{B}) = G$

Proof

Step	Hyp	Ref	Expression
1		updjud.f	$⊢ φ \to F : A ⟶ C$
2		updjud.g	$⊢ φ \to G : B ⟶ C$
3		updjudhf.h	$⊢ H = (x \in (A ⊔︀ B) ⟼ if (1^{st} (x) = \emptyset, F (2^{nd} (x)), G (2^{nd} (x))))$
4	1 2 3	updjudhf	$⊢ φ \to H : (A ⊔︀ B) ⟶ C$
5	4	ffnd	$⊢ φ \to H Fn (A ⊔︀ B)$
6		inrresf	$⊢ ({inr ↾}_{B}) : B ⟶ (A ⊔︀ B)$
7		ffn	$⊢ ({inr ↾}_{B}) : B ⟶ (A ⊔︀ B) \to ({inr ↾}_{B}) Fn B$
8	6 7	mp1i	$⊢ φ \to ({inr ↾}_{B}) Fn B$
9		frn	$⊢ ({inr ↾}_{B}) : B ⟶ (A ⊔︀ B) \to ran ({inr ↾}_{B}) \subseteq (A ⊔︀ B)$
10	6 9	mp1i	$⊢ φ \to ran ({inr ↾}_{B}) \subseteq (A ⊔︀ B)$
11		fnco	$⊢ (H Fn (A ⊔︀ B) \land ({inr ↾}_{B}) Fn B \land ran ({inr ↾}_{B}) \subseteq (A ⊔︀ B)) \to (H \circ ({inr ↾}_{B})) Fn B$
12	5 8 10 11	syl3anc	$⊢ φ \to (H \circ ({inr ↾}_{B})) Fn B$
13	2	ffnd	$⊢ φ \to G Fn B$
14		fvco2	$⊢ (({inr ↾}_{B}) Fn B \land b \in B) \to (H \circ ({inr ↾}_{B})) (b) = H (({inr ↾}_{B}) (b))$
15	8 14	sylan	$⊢ (φ \land b \in B) \to (H \circ ({inr ↾}_{B})) (b) = H (({inr ↾}_{B}) (b))$
16		fvres	$⊢ b \in B \to ({inr ↾}_{B}) (b) = inr (b)$
17	16	adantl	$⊢ (φ \land b \in B) \to ({inr ↾}_{B}) (b) = inr (b)$
18	17	fveq2d	$⊢ (φ \land b \in B) \to H (({inr ↾}_{B}) (b)) = H (inr (b))$
19		fveqeq2	$⊢ x = inr (b) \to (1^{st} (x) = \emptyset \leftrightarrow 1^{st} (inr (b)) = \emptyset)$
20		2fveq3	$⊢ x = inr (b) \to F (2^{nd} (x)) = F (2^{nd} (inr (b)))$
21		2fveq3	$⊢ x = inr (b) \to G (2^{nd} (x)) = G (2^{nd} (inr (b)))$
22	19 20 21	ifbieq12d	$⊢ x = inr (b) \to if (1^{st} (x) = \emptyset, F (2^{nd} (x)), G (2^{nd} (x))) = if (1^{st} (inr (b)) = \emptyset, F (2^{nd} (inr (b))), G (2^{nd} (inr (b))))$
23	22	adantl	$⊢ ((φ \land b \in B) \land x = inr (b)) \to if (1^{st} (x) = \emptyset, F (2^{nd} (x)), G (2^{nd} (x))) = if (1^{st} (inr (b)) = \emptyset, F (2^{nd} (inr (b))), G (2^{nd} (inr (b))))$
24		1stinr	$⊢ b \in B \to 1^{st} (inr (b)) = 1_{𝑜}$
25		1n0	$⊢ 1_{𝑜} \neq \emptyset$
26	25	neii	$⊢ \neg 1_{𝑜} = \emptyset$
27		eqeq1	$⊢ 1^{st} (inr (b)) = 1_{𝑜} \to (1^{st} (inr (b)) = \emptyset \leftrightarrow 1_{𝑜} = \emptyset)$
28	26 27	mtbiri	$⊢ 1^{st} (inr (b)) = 1_{𝑜} \to \neg 1^{st} (inr (b)) = \emptyset$
29	24 28	syl	$⊢ b \in B \to \neg 1^{st} (inr (b)) = \emptyset$
30	29	adantl	$⊢ (φ \land b \in B) \to \neg 1^{st} (inr (b)) = \emptyset$
31	30	adantr	$⊢ ((φ \land b \in B) \land x = inr (b)) \to \neg 1^{st} (inr (b)) = \emptyset$
32	31	iffalsed	$⊢ ((φ \land b \in B) \land x = inr (b)) \to if (1^{st} (inr (b)) = \emptyset, F (2^{nd} (inr (b))), G (2^{nd} (inr (b)))) = G (2^{nd} (inr (b)))$
33	23 32	eqtrd	$⊢ ((φ \land b \in B) \land x = inr (b)) \to if (1^{st} (x) = \emptyset, F (2^{nd} (x)), G (2^{nd} (x))) = G (2^{nd} (inr (b)))$
34		djurcl	$⊢ b \in B \to inr (b) \in (A ⊔︀ B)$
35	34	adantl	$⊢ (φ \land b \in B) \to inr (b) \in (A ⊔︀ B)$
36	2	adantr	$⊢ (φ \land b \in B) \to G : B ⟶ C$
37		2ndinr	$⊢ b \in B \to 2^{nd} (inr (b)) = b$
38	37	adantl	$⊢ (φ \land b \in B) \to 2^{nd} (inr (b)) = b$
39		simpr	$⊢ (φ \land b \in B) \to b \in B$
40	38 39	eqeltrd	$⊢ (φ \land b \in B) \to 2^{nd} (inr (b)) \in B$
41	36 40	ffvelcdmd	$⊢ (φ \land b \in B) \to G (2^{nd} (inr (b))) \in C$
42	3 33 35 41	fvmptd2	$⊢ (φ \land b \in B) \to H (inr (b)) = G (2^{nd} (inr (b)))$
43	18 42	eqtrd	$⊢ (φ \land b \in B) \to H (({inr ↾}_{B}) (b)) = G (2^{nd} (inr (b)))$
44	38	fveq2d	$⊢ (φ \land b \in B) \to G (2^{nd} (inr (b))) = G (b)$
45	15 43 44	3eqtrd	$⊢ (φ \land b \in B) \to (H \circ ({inr ↾}_{B})) (b) = G (b)$
46	12 13 45	eqfnfvd	$⊢ φ \to H \circ ({inr ↾}_{B}) = G$

Metamath Proof Explorer

Theorem updjudhcoinrg

Proof