functhinclem1

Description: Lemma for functhinc . Given the object part, there is only one possible morphism part such that the mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	functhinclem1.b	$⊢ B = {Base}_{D}$
	functhinclem1.c	$⊢ C = {Base}_{E}$
	functhinclem1.h	$⊢ H = Hom (D)$
	functhinclem1.j	$⊢ J = Hom (E)$
	functhinclem1.e	No typesetting found for \|- ( ph -> E e. ThinCat ) with typecode \|-
	functhinclem1.f	$⊢ φ \to F : B ⟶ C$
	functhinclem1.k	$⊢ K = (x \in B, y \in B ⟼ (x H y) \times (F (x) J F (y)))$
	functhinclem1.1	$⊢ (φ \land (z \in B \land w \in B)) \to (F (z) J F (w) = \emptyset \to z H w = \emptyset)$
Assertion	functhinclem1	$⊢ φ \to ((G \in V \land G Fn (B \times B) \land \forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w)) \leftrightarrow G = K)$

Proof

Step	Hyp	Ref	Expression
1		functhinclem1.b	$⊢ B = {Base}_{D}$
2		functhinclem1.c	$⊢ C = {Base}_{E}$
3		functhinclem1.h	$⊢ H = Hom (D)$
4		functhinclem1.j	$⊢ J = Hom (E)$
5		functhinclem1.e	Could not format ( ph -> E e. ThinCat ) : No typesetting found for \|- ( ph -> E e. ThinCat ) with typecode \|-
6		functhinclem1.f	$⊢ φ \to F : B ⟶ C$
7		functhinclem1.k	$⊢ K = (x \in B, y \in B ⟼ (x H y) \times (F (x) J F (y)))$
8		functhinclem1.1	$⊢ (φ \land (z \in B \land w \in B)) \to (F (z) J F (w) = \emptyset \to z H w = \emptyset)$
9		simpl	$⊢ (φ \land (G \in V \land G Fn (B \times B) \land \forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w))) \to φ$
10		simpr2	$⊢ (φ \land (G \in V \land G Fn (B \times B) \land \forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w))) \to G Fn (B \times B)$
11		simpr3	$⊢ (φ \land (G \in V \land G Fn (B \times B) \land \forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w))) \to \forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w)$
12		eqid	$⊢ (z H w) \times (F (z) J F (w)) = (z H w) \times (F (z) J F (w))$
13	8	adantlr	$⊢ ((φ \land G Fn (B \times B)) \land (z \in B \land w \in B)) \to (F (z) J F (w) = \emptyset \to z H w = \emptyset)$
14	5	ad2antrr	Could not format ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> E e. ThinCat ) : No typesetting found for \|- ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> E e. ThinCat ) with typecode \|-
15	6	ad2antrr	$⊢ ((φ \land G Fn (B \times B)) \land (z \in B \land w \in B)) \to F : B ⟶ C$
16		simprl	$⊢ ((φ \land G Fn (B \times B)) \land (z \in B \land w \in B)) \to z \in B$
17	15 16	ffvelrnd	$⊢ ((φ \land G Fn (B \times B)) \land (z \in B \land w \in B)) \to F (z) \in C$
18		simprr	$⊢ ((φ \land G Fn (B \times B)) \land (z \in B \land w \in B)) \to w \in B$
19	15 18	ffvelrnd	$⊢ ((φ \land G Fn (B \times B)) \land (z \in B \land w \in B)) \to F (w) \in C$
20	14 17 19 2 4	thincmo	$⊢ ((φ \land G Fn (B \times B)) \land (z \in B \land w \in B)) \to \exists^{*} m m \in (F (z) J F (w))$
21	12 13 20	mofeu	$⊢ ((φ \land G Fn (B \times B)) \land (z \in B \land w \in B)) \to ((z G w) : z H w ⟶ F (z) J F (w) \leftrightarrow z G w = (z H w) \times (F (z) J F (w)))$
22		oveq1	$⊢ x = z \to x H y = z H y$
23		fveq2	$⊢ x = z \to F (x) = F (z)$
24	23	oveq1d	$⊢ x = z \to F (x) J F (y) = F (z) J F (y)$
25	22 24	xpeq12d	$⊢ x = z \to (x H y) \times (F (x) J F (y)) = (z H y) \times (F (z) J F (y))$
26		oveq2	$⊢ y = w \to z H y = z H w$
27		fveq2	$⊢ y = w \to F (y) = F (w)$
28	27	oveq2d	$⊢ y = w \to F (z) J F (y) = F (z) J F (w)$
29	26 28	xpeq12d	$⊢ y = w \to (z H y) \times (F (z) J F (y)) = (z H w) \times (F (z) J F (w))$
30		ovex	$⊢ z H w \in V$
31		ovex	$⊢ F (z) J F (w) \in V$
32	30 31	xpex	$⊢ (z H w) \times (F (z) J F (w)) \in V$
33	25 29 7 32	ovmpo	$⊢ (z \in B \land w \in B) \to z K w = (z H w) \times (F (z) J F (w))$
34	33	adantl	$⊢ ((φ \land G Fn (B \times B)) \land (z \in B \land w \in B)) \to z K w = (z H w) \times (F (z) J F (w))$
35	34	eqeq2d	$⊢ ((φ \land G Fn (B \times B)) \land (z \in B \land w \in B)) \to (z G w = z K w \leftrightarrow z G w = (z H w) \times (F (z) J F (w)))$
36	21 35	bitr4d	$⊢ ((φ \land G Fn (B \times B)) \land (z \in B \land w \in B)) \to ((z G w) : z H w ⟶ F (z) J F (w) \leftrightarrow z G w = z K w)$
37	36	2ralbidva	$⊢ (φ \land G Fn (B \times B)) \to (\forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w) \leftrightarrow \forall z \in B \forall w \in B z G w = z K w)$
38		simpr	$⊢ (φ \land G Fn (B \times B)) \to G Fn (B \times B)$
39		ovex	$⊢ x H y \in V$
40		ovex	$⊢ F (x) J F (y) \in V$
41	39 40	xpex	$⊢ (x H y) \times (F (x) J F (y)) \in V$
42	7 41	fnmpoi	$⊢ K Fn (B \times B)$
43		eqfnov2	$⊢ (G Fn (B \times B) \land K Fn (B \times B)) \to (G = K \leftrightarrow \forall z \in B \forall w \in B z G w = z K w)$
44	38 42 43	sylancl	$⊢ (φ \land G Fn (B \times B)) \to (G = K \leftrightarrow \forall z \in B \forall w \in B z G w = z K w)$
45	37 44	bitr4d	$⊢ (φ \land G Fn (B \times B)) \to (\forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w) \leftrightarrow G = K)$
46	45	biimpa	$⊢ ((φ \land G Fn (B \times B)) \land \forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w)) \to G = K$
47	9 10 11 46	syl21anc	$⊢ (φ \land (G \in V \land G Fn (B \times B) \land \forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w))) \to G = K$
48	1	fvexi	$⊢ B \in V$
49	48 48	mpoex	$⊢ (x \in B, y \in B ⟼ (x H y) \times (F (x) J F (y))) \in V$
50	7 49	eqeltri	$⊢ K \in V$
51		eleq1	$⊢ G = K \to (G \in V \leftrightarrow K \in V)$
52	50 51	mpbiri	$⊢ G = K \to G \in V$
53	52	adantl	$⊢ (φ \land G = K) \to G \in V$
54		fneq1	$⊢ G = K \to (G Fn (B \times B) \leftrightarrow K Fn (B \times B))$
55	42 54	mpbiri	$⊢ G = K \to G Fn (B \times B)$
56	55	adantl	$⊢ (φ \land G = K) \to G Fn (B \times B)$
57		simpl	$⊢ (φ \land G = K) \to φ$
58		simpr	$⊢ (φ \land G = K) \to G = K$
59	45	biimpar	$⊢ ((φ \land G Fn (B \times B)) \land G = K) \to \forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w)$
60	57 56 58 59	syl21anc	$⊢ (φ \land G = K) \to \forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w)$
61	53 56 60	3jca	$⊢ (φ \land G = K) \to (G \in V \land G Fn (B \times B) \land \forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w))$
62	47 61	impbida	$⊢ φ \to ((G \in V \land G Fn (B \times B) \land \forall z \in B \forall w \in B (z G w) : z H w ⟶ F (z) J F (w)) \leftrightarrow G = K)$

Metamath Proof Explorer

Theorem functhinclem1

Proof