functhinclem3

Description: Lemma for functhinc . The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	functhinclem3.x	$⊢ φ \to X \in B$
	functhinclem3.y	$⊢ φ \to Y \in B$
	functhinclem3.m	$⊢ φ \to M \in (X H Y)$
	functhinclem3.g	$⊢ φ \to G = (x \in B, y \in B ⟼ (x H y) \times (F (x) J F (y)))$
	functhinclem3.1	$⊢ φ \to (F (X) J F (Y) = \emptyset \to X H Y = \emptyset)$
	functhinclem3.2	$⊢ φ \to \exists^{*} n n \in (F (X) J F (Y))$
Assertion	functhinclem3	$⊢ φ \to (X G Y) (M) \in (F (X) J F (Y))$

Step	Hyp	Ref	Expression
1		functhinclem3.x	$⊢ φ \to X \in B$
2		functhinclem3.y	$⊢ φ \to Y \in B$
3		functhinclem3.m	$⊢ φ \to M \in (X H Y)$
4		functhinclem3.g	$⊢ φ \to G = (x \in B, y \in B ⟼ (x H y) \times (F (x) J F (y)))$
5		functhinclem3.1	$⊢ φ \to (F (X) J F (Y) = \emptyset \to X H Y = \emptyset)$
6		functhinclem3.2	$⊢ φ \to \exists^{*} n n \in (F (X) J F (Y))$
7		simprl	$⊢ (φ \land (x = X \land y = Y)) \to x = X$
8		simprr	$⊢ (φ \land (x = X \land y = Y)) \to y = Y$
9	7 8	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to x H y = X H Y$
10	7	fveq2d	$⊢ (φ \land (x = X \land y = Y)) \to F (x) = F (X)$
11	8	fveq2d	$⊢ (φ \land (x = X \land y = Y)) \to F (y) = F (Y)$
12	10 11	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to F (x) J F (y) = F (X) J F (Y)$
13	9 12	xpeq12d	$⊢ (φ \land (x = X \land y = Y)) \to (x H y) \times (F (x) J F (y)) = (X H Y) \times (F (X) J F (Y))$
14		ovex	$⊢ X H Y \in V$
15		ovex	$⊢ F (X) J F (Y) \in V$
16	14 15	xpex	$⊢ (X H Y) \times (F (X) J F (Y)) \in V$
17	16	a1i	$⊢ φ \to (X H Y) \times (F (X) J F (Y)) \in V$
18	4 13 1 2 17	ovmpod	$⊢ φ \to X G Y = (X H Y) \times (F (X) J F (Y))$
19		eqid	$⊢ (X H Y) \times (F (X) J F (Y)) = (X H Y) \times (F (X) J F (Y))$
20	19 5 6	mofeu	$⊢ φ \to ((X G Y) : X H Y ⟶ F (X) J F (Y) \leftrightarrow X G Y = (X H Y) \times (F (X) J F (Y)))$
21	18 20	mpbird	$⊢ φ \to (X G Y) : X H Y ⟶ F (X) J F (Y)$
22	21 3	ffvelrnd	$⊢ φ \to (X G Y) (M) \in (F (X) J F (Y))$

Metamath Proof Explorer