cat1lem

Description: The category of sets in a "universe" containing the empty set and another set does not have pairwise disjoint hom-sets as required in Axiom CAT 1 in Lang p. 53. Lemma for cat1 . (Contributed by Zhi Wang, 15-Sep-2024)

	Ref	Expression
Hypotheses	cat1lem.1	$⊢ C = SetCat (U)$
	cat1lem.2	$⊢ φ \to U \in V$
	cat1lem.3	$⊢ B = {Base}_{C}$
	cat1lem.4	$⊢ H = Hom (C)$
	cat1lem.5	$⊢ φ \to \emptyset \in U$
	cat1lem.6	$⊢ φ \to Y \in U$
	cat1lem.7	$⊢ φ \to \emptyset \neq Y$
Assertion	cat1lem	$⊢ φ \to \exists x \in B \exists y \in B \exists z \in B \exists w \in B ((x H y) \cap (z H w) \neq \emptyset \land \neg (x = z \land y = w))$

Proof

Step	Hyp	Ref	Expression
1		cat1lem.1	$⊢ C = SetCat (U)$
2		cat1lem.2	$⊢ φ \to U \in V$
3		cat1lem.3	$⊢ B = {Base}_{C}$
4		cat1lem.4	$⊢ H = Hom (C)$
5		cat1lem.5	$⊢ φ \to \emptyset \in U$
6		cat1lem.6	$⊢ φ \to Y \in U$
7		cat1lem.7	$⊢ φ \to \emptyset \neq Y$
8	1 2	setcbas	$⊢ φ \to U = {Base}_{C}$
9	8 3	eqtr4di	$⊢ φ \to U = B$
10	5 9	eleqtrd	$⊢ φ \to \emptyset \in B$
11	6 9	eleqtrd	$⊢ φ \to Y \in B$
12		f0	$⊢ \emptyset : \emptyset ⟶ \emptyset$
13	1 2 4 5 5	elsetchom	$⊢ φ \to (\emptyset \in (\emptyset H \emptyset) \leftrightarrow \emptyset : \emptyset ⟶ \emptyset)$
14	12 13	mpbiri	$⊢ φ \to \emptyset \in (\emptyset H \emptyset)$
15		f0	$⊢ \emptyset : \emptyset ⟶ Y$
16	1 2 4 5 6	elsetchom	$⊢ φ \to (\emptyset \in (\emptyset H Y) \leftrightarrow \emptyset : \emptyset ⟶ Y)$
17	15 16	mpbiri	$⊢ φ \to \emptyset \in (\emptyset H Y)$
18		inelcm	$⊢ (\emptyset \in (\emptyset H \emptyset) \land \emptyset \in (\emptyset H Y)) \to (\emptyset H \emptyset) \cap (\emptyset H Y) \neq \emptyset$
19	14 17 18	syl2anc	$⊢ φ \to (\emptyset H \emptyset) \cap (\emptyset H Y) \neq \emptyset$
20	7	neneqd	$⊢ φ \to \neg \emptyset = Y$
21	20	intnand	$⊢ φ \to \neg (\emptyset = \emptyset \land \emptyset = Y)$
22		oveq1	$⊢ z = \emptyset \to z H w = \emptyset H w$
23	22	ineq2d	$⊢ z = \emptyset \to (\emptyset H \emptyset) \cap (z H w) = (\emptyset H \emptyset) \cap (\emptyset H w)$
24	23	neeq1d	$⊢ z = \emptyset \to ((\emptyset H \emptyset) \cap (z H w) \neq \emptyset \leftrightarrow (\emptyset H \emptyset) \cap (\emptyset H w) \neq \emptyset)$
25		eqeq2	$⊢ z = \emptyset \to (\emptyset = z \leftrightarrow \emptyset = \emptyset)$
26	25	anbi1d	$⊢ z = \emptyset \to ((\emptyset = z \land \emptyset = w) \leftrightarrow (\emptyset = \emptyset \land \emptyset = w))$
27	26	notbid	$⊢ z = \emptyset \to (\neg (\emptyset = z \land \emptyset = w) \leftrightarrow \neg (\emptyset = \emptyset \land \emptyset = w))$
28	24 27	anbi12d	$⊢ z = \emptyset \to (((\emptyset H \emptyset) \cap (z H w) \neq \emptyset \land \neg (\emptyset = z \land \emptyset = w)) \leftrightarrow ((\emptyset H \emptyset) \cap (\emptyset H w) \neq \emptyset \land \neg (\emptyset = \emptyset \land \emptyset = w)))$
29		oveq2	$⊢ w = Y \to \emptyset H w = \emptyset H Y$
30	29	ineq2d	$⊢ w = Y \to (\emptyset H \emptyset) \cap (\emptyset H w) = (\emptyset H \emptyset) \cap (\emptyset H Y)$
31	30	neeq1d	$⊢ w = Y \to ((\emptyset H \emptyset) \cap (\emptyset H w) \neq \emptyset \leftrightarrow (\emptyset H \emptyset) \cap (\emptyset H Y) \neq \emptyset)$
32		eqeq2	$⊢ w = Y \to (\emptyset = w \leftrightarrow \emptyset = Y)$
33	32	anbi2d	$⊢ w = Y \to ((\emptyset = \emptyset \land \emptyset = w) \leftrightarrow (\emptyset = \emptyset \land \emptyset = Y))$
34	33	notbid	$⊢ w = Y \to (\neg (\emptyset = \emptyset \land \emptyset = w) \leftrightarrow \neg (\emptyset = \emptyset \land \emptyset = Y))$
35	31 34	anbi12d	$⊢ w = Y \to (((\emptyset H \emptyset) \cap (\emptyset H w) \neq \emptyset \land \neg (\emptyset = \emptyset \land \emptyset = w)) \leftrightarrow ((\emptyset H \emptyset) \cap (\emptyset H Y) \neq \emptyset \land \neg (\emptyset = \emptyset \land \emptyset = Y)))$
36	28 35	rspc2ev	$⊢ (\emptyset \in B \land Y \in B \land ((\emptyset H \emptyset) \cap (\emptyset H Y) \neq \emptyset \land \neg (\emptyset = \emptyset \land \emptyset = Y))) \to \exists z \in B \exists w \in B ((\emptyset H \emptyset) \cap (z H w) \neq \emptyset \land \neg (\emptyset = z \land \emptyset = w))$
37	10 11 19 21 36	syl112anc	$⊢ φ \to \exists z \in B \exists w \in B ((\emptyset H \emptyset) \cap (z H w) \neq \emptyset \land \neg (\emptyset = z \land \emptyset = w))$
38		oveq1	$⊢ x = \emptyset \to x H y = \emptyset H y$
39	38	ineq1d	$⊢ x = \emptyset \to (x H y) \cap (z H w) = (\emptyset H y) \cap (z H w)$
40	39	neeq1d	$⊢ x = \emptyset \to ((x H y) \cap (z H w) \neq \emptyset \leftrightarrow (\emptyset H y) \cap (z H w) \neq \emptyset)$
41		eqeq1	$⊢ x = \emptyset \to (x = z \leftrightarrow \emptyset = z)$
42	41	anbi1d	$⊢ x = \emptyset \to ((x = z \land y = w) \leftrightarrow (\emptyset = z \land y = w))$
43	42	notbid	$⊢ x = \emptyset \to (\neg (x = z \land y = w) \leftrightarrow \neg (\emptyset = z \land y = w))$
44	40 43	anbi12d	$⊢ x = \emptyset \to (((x H y) \cap (z H w) \neq \emptyset \land \neg (x = z \land y = w)) \leftrightarrow ((\emptyset H y) \cap (z H w) \neq \emptyset \land \neg (\emptyset = z \land y = w)))$
45	44	2rexbidv	$⊢ x = \emptyset \to (\exists z \in B \exists w \in B ((x H y) \cap (z H w) \neq \emptyset \land \neg (x = z \land y = w)) \leftrightarrow \exists z \in B \exists w \in B ((\emptyset H y) \cap (z H w) \neq \emptyset \land \neg (\emptyset = z \land y = w)))$
46		oveq2	$⊢ y = \emptyset \to \emptyset H y = \emptyset H \emptyset$
47	46	ineq1d	$⊢ y = \emptyset \to (\emptyset H y) \cap (z H w) = (\emptyset H \emptyset) \cap (z H w)$
48	47	neeq1d	$⊢ y = \emptyset \to ((\emptyset H y) \cap (z H w) \neq \emptyset \leftrightarrow (\emptyset H \emptyset) \cap (z H w) \neq \emptyset)$
49		eqeq1	$⊢ y = \emptyset \to (y = w \leftrightarrow \emptyset = w)$
50	49	anbi2d	$⊢ y = \emptyset \to ((\emptyset = z \land y = w) \leftrightarrow (\emptyset = z \land \emptyset = w))$
51	50	notbid	$⊢ y = \emptyset \to (\neg (\emptyset = z \land y = w) \leftrightarrow \neg (\emptyset = z \land \emptyset = w))$
52	48 51	anbi12d	$⊢ y = \emptyset \to (((\emptyset H y) \cap (z H w) \neq \emptyset \land \neg (\emptyset = z \land y = w)) \leftrightarrow ((\emptyset H \emptyset) \cap (z H w) \neq \emptyset \land \neg (\emptyset = z \land \emptyset = w)))$
53	52	2rexbidv	$⊢ y = \emptyset \to (\exists z \in B \exists w \in B ((\emptyset H y) \cap (z H w) \neq \emptyset \land \neg (\emptyset = z \land y = w)) \leftrightarrow \exists z \in B \exists w \in B ((\emptyset H \emptyset) \cap (z H w) \neq \emptyset \land \neg (\emptyset = z \land \emptyset = w)))$
54	45 53	rspc2ev	$⊢ (\emptyset \in B \land \emptyset \in B \land \exists z \in B \exists w \in B ((\emptyset H \emptyset) \cap (z H w) \neq \emptyset \land \neg (\emptyset = z \land \emptyset = w))) \to \exists x \in B \exists y \in B \exists z \in B \exists w \in B ((x H y) \cap (z H w) \neq \emptyset \land \neg (x = z \land y = w))$
55	10 10 37 54	syl3anc	$⊢ φ \to \exists x \in B \exists y \in B \exists z \in B \exists w \in B ((x H y) \cap (z H w) \neq \emptyset \land \neg (x = z \land y = w))$

Metamath Proof Explorer

Theorem cat1lem

Proof