Theorem 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	⊢ 𝐶 = ( SetCat ‘ 𝑈 )
	cat1lem.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	cat1lem.3	⊢ 𝐵 = ( Base ‘ 𝐶 )
	cat1lem.4	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	cat1lem.5	⊢ ( 𝜑 → ∅ ∈ 𝑈 )
	cat1lem.6	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
	cat1lem.7	⊢ ( 𝜑 → ∅ ≠ 𝑌 )
Assertion	cat1lem	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cat1lem.1	⊢ 𝐶 = ( SetCat ‘ 𝑈 )
2		cat1lem.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		cat1lem.3	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		cat1lem.4	⊢ 𝐻 = ( Hom ‘ 𝐶 )
5		cat1lem.5	⊢ ( 𝜑 → ∅ ∈ 𝑈 )
6		cat1lem.6	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
7		cat1lem.7	⊢ ( 𝜑 → ∅ ≠ 𝑌 )
8	1 2	setcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐶 ) )
9	8 3	eqtr4di	⊢ ( 𝜑 → 𝑈 = 𝐵 )
10	5 9	eleqtrd	⊢ ( 𝜑 → ∅ ∈ 𝐵 )
11	6 9	eleqtrd	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
12		f0	⊢ ∅ : ∅ ⟶ ∅
13	1 2 4 5 5	elsetchom	⊢ ( 𝜑 → ( ∅ ∈ ( ∅ 𝐻 ∅ ) ↔ ∅ : ∅ ⟶ ∅ ) )
14	12 13	mpbiri	⊢ ( 𝜑 → ∅ ∈ ( ∅ 𝐻 ∅ ) )
15		f0	⊢ ∅ : ∅ ⟶ 𝑌
16	1 2 4 5 6	elsetchom	⊢ ( 𝜑 → ( ∅ ∈ ( ∅ 𝐻 𝑌 ) ↔ ∅ : ∅ ⟶ 𝑌 ) )
17	15 16	mpbiri	⊢ ( 𝜑 → ∅ ∈ ( ∅ 𝐻 𝑌 ) )
18		inelcm	⊢ ( ( ∅ ∈ ( ∅ 𝐻 ∅ ) ∧ ∅ ∈ ( ∅ 𝐻 𝑌 ) ) → ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑌 ) ) ≠ ∅ )
19	14 17 18	syl2anc	⊢ ( 𝜑 → ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑌 ) ) ≠ ∅ )
20	7	neneqd	⊢ ( 𝜑 → ¬ ∅ = 𝑌 )
21	20	intnand	⊢ ( 𝜑 → ¬ ( ∅ = ∅ ∧ ∅ = 𝑌 ) )
22		oveq1	⊢ ( 𝑧 = ∅ → ( 𝑧 𝐻 𝑤 ) = ( ∅ 𝐻 𝑤 ) )
23	22	ineq2d	⊢ ( 𝑧 = ∅ → ( ( ∅ 𝐻 ∅ ) ∩ ( 𝑧 𝐻 𝑤 ) ) = ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑤 ) ) )
24	23	neeq1d	⊢ ( 𝑧 = ∅ → ( ( ( ∅ 𝐻 ∅ ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ↔ ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑤 ) ) ≠ ∅ ) )
25		eqeq2	⊢ ( 𝑧 = ∅ → ( ∅ = 𝑧 ↔ ∅ = ∅ ) )
26	25	anbi1d	⊢ ( 𝑧 = ∅ → ( ( ∅ = 𝑧 ∧ ∅ = 𝑤 ) ↔ ( ∅ = ∅ ∧ ∅ = 𝑤 ) ) )
27	26	notbid	⊢ ( 𝑧 = ∅ → ( ¬ ( ∅ = 𝑧 ∧ ∅ = 𝑤 ) ↔ ¬ ( ∅ = ∅ ∧ ∅ = 𝑤 ) ) )
28	24 27	anbi12d	⊢ ( 𝑧 = ∅ → ( ( ( ( ∅ 𝐻 ∅ ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = 𝑧 ∧ ∅ = 𝑤 ) ) ↔ ( ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = ∅ ∧ ∅ = 𝑤 ) ) ) )
29		oveq2	⊢ ( 𝑤 = 𝑌 → ( ∅ 𝐻 𝑤 ) = ( ∅ 𝐻 𝑌 ) )
30	29	ineq2d	⊢ ( 𝑤 = 𝑌 → ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑤 ) ) = ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑌 ) ) )
31	30	neeq1d	⊢ ( 𝑤 = 𝑌 → ( ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑤 ) ) ≠ ∅ ↔ ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑌 ) ) ≠ ∅ ) )
32		eqeq2	⊢ ( 𝑤 = 𝑌 → ( ∅ = 𝑤 ↔ ∅ = 𝑌 ) )
33	32	anbi2d	⊢ ( 𝑤 = 𝑌 → ( ( ∅ = ∅ ∧ ∅ = 𝑤 ) ↔ ( ∅ = ∅ ∧ ∅ = 𝑌 ) ) )
34	33	notbid	⊢ ( 𝑤 = 𝑌 → ( ¬ ( ∅ = ∅ ∧ ∅ = 𝑤 ) ↔ ¬ ( ∅ = ∅ ∧ ∅ = 𝑌 ) ) )
35	31 34	anbi12d	⊢ ( 𝑤 = 𝑌 → ( ( ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = ∅ ∧ ∅ = 𝑤 ) ) ↔ ( ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑌 ) ) ≠ ∅ ∧ ¬ ( ∅ = ∅ ∧ ∅ = 𝑌 ) ) ) )
36	28 35	rspc2ev	⊢ ( ( ∅ ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( ∅ 𝐻 ∅ ) ∩ ( ∅ 𝐻 𝑌 ) ) ≠ ∅ ∧ ¬ ( ∅ = ∅ ∧ ∅ = 𝑌 ) ) ) → ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( ( ∅ 𝐻 ∅ ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = 𝑧 ∧ ∅ = 𝑤 ) ) )
37	10 11 19 21 36	syl112anc	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( ( ∅ 𝐻 ∅ ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = 𝑧 ∧ ∅ = 𝑤 ) ) )
38		oveq1	⊢ ( 𝑥 = ∅ → ( 𝑥 𝐻 𝑦 ) = ( ∅ 𝐻 𝑦 ) )
39	38	ineq1d	⊢ ( 𝑥 = ∅ → ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) = ( ( ∅ 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) )
40	39	neeq1d	⊢ ( 𝑥 = ∅ → ( ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ↔ ( ( ∅ 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ) )
41		eqeq1	⊢ ( 𝑥 = ∅ → ( 𝑥 = 𝑧 ↔ ∅ = 𝑧 ) )
42	41	anbi1d	⊢ ( 𝑥 = ∅ → ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ↔ ( ∅ = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
43	42	notbid	⊢ ( 𝑥 = ∅ → ( ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ↔ ¬ ( ∅ = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
44	40 43	anbi12d	⊢ ( 𝑥 = ∅ → ( ( ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( ( ( ∅ 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
45	44	2rexbidv	⊢ ( 𝑥 = ∅ → ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( ( ∅ 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
46		oveq2	⊢ ( 𝑦 = ∅ → ( ∅ 𝐻 𝑦 ) = ( ∅ 𝐻 ∅ ) )
47	46	ineq1d	⊢ ( 𝑦 = ∅ → ( ( ∅ 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) = ( ( ∅ 𝐻 ∅ ) ∩ ( 𝑧 𝐻 𝑤 ) ) )
48	47	neeq1d	⊢ ( 𝑦 = ∅ → ( ( ( ∅ 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ↔ ( ( ∅ 𝐻 ∅ ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ) )
49		eqeq1	⊢ ( 𝑦 = ∅ → ( 𝑦 = 𝑤 ↔ ∅ = 𝑤 ) )
50	49	anbi2d	⊢ ( 𝑦 = ∅ → ( ( ∅ = 𝑧 ∧ 𝑦 = 𝑤 ) ↔ ( ∅ = 𝑧 ∧ ∅ = 𝑤 ) ) )
51	50	notbid	⊢ ( 𝑦 = ∅ → ( ¬ ( ∅ = 𝑧 ∧ 𝑦 = 𝑤 ) ↔ ¬ ( ∅ = 𝑧 ∧ ∅ = 𝑤 ) ) )
52	48 51	anbi12d	⊢ ( 𝑦 = ∅ → ( ( ( ( ∅ 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( ( ( ∅ 𝐻 ∅ ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = 𝑧 ∧ ∅ = 𝑤 ) ) ) )
53	52	2rexbidv	⊢ ( 𝑦 = ∅ → ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( ( ∅ 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( ( ∅ 𝐻 ∅ ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = 𝑧 ∧ ∅ = 𝑤 ) ) ) )
54	45 53	rspc2ev	⊢ ( ( ∅ ∈ 𝐵 ∧ ∅ ∈ 𝐵 ∧ ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( ( ∅ 𝐻 ∅ ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( ∅ = 𝑧 ∧ ∅ = 𝑤 ) ) ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
55	10 10 37 54	syl3anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( ( 𝑥 𝐻 𝑦 ) ∩ ( 𝑧 𝐻 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )