iinfsubc - Mathbox for Zhi Wang

	Mathbox for Zhi Wang		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > iinfsubc		Structured version Visualization version GIF version

Theorem iinfsubc 49548

Description: Indexed intersection of subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.)

**Hypotheses**
Ref	Expression
iinfsubc.1	⊢ (𝜑 → 𝐴 ≠ ∅)
iinfsubc.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ∈ (Subcat‘𝐶))
iinfsubc.3	⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))

**Assertion**
Ref	Expression
iinfsubc	⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐶))

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐶 𝑦,𝐻 𝜑,𝑥,𝑦 Allowed substitution hints: 𝐶(𝑦) 𝐻(𝑥) 𝐾(𝑥,𝑦)

Proof of Theorem iinfsubc Dummy variables 𝑎 𝑏 𝑐 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iinfsubc.1	. . 3 ⊢ (𝜑 → 𝐴 ≠ ∅)
2		iinfsubc.2	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ∈ (Subcat‘𝐶))
3		eqid 2737	. . . 4 ⊢ (Hom_f ‘𝐶) = (Hom_f ‘𝐶)
4	2, 3	subcssc 17801	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
5		iinfsubc.3	. . 3 ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
6	1, 4, 5	iinfssc 49547	. 2 ⊢ (𝜑 → 𝐾 ⊆_cat (Hom_f ‘𝐶))
7	2	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → 𝐻 ∈ (Subcat‘𝐶))
8		eqidd 2738	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
9	2, 8	subcfn 17802	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
10	9	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
11		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → 𝑎 ∈ dom dom 𝐻)
12		eqid 2737	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
13	7, 10, 11, 12	subcidcl 17805	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎))
14	13	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑎 ∈ dom dom 𝐻 → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
15	14	ralimdva 3150	. . . . . . 7 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻 → ∀𝑥 ∈ 𝐴 ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
16		eliin 4939	. . . . . . . 8 ⊢ (𝑎 ∈ V → (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻))
17	16	elv 3435	. . . . . . 7 ⊢ (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻)
18		fvex 6848	. . . . . . . 8 ⊢ ((Id‘𝐶)‘𝑎) ∈ V
19		eliin 4939	. . . . . . . 8 ⊢ (((Id‘𝐶)‘𝑎) ∈ V → (((Id‘𝐶)‘𝑎) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎) ↔ ∀𝑥 ∈ 𝐴 ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
20	18, 19	ax-mp 5	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑎) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎) ↔ ∀𝑥 ∈ 𝐴 ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎))
21	15, 17, 20	3imtr4g 296	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 → ((Id‘𝐶)‘𝑎) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎)))
22	21	imp 406	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎))
23	1	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → 𝐴 ≠ ∅)
24	4	adantlr 716	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
25	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
26		eqidd 2738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
27		nfv 1916	. . . . . . 7 ⊢ Ⅎ𝑥𝜑
28		nfii1 4972	. . . . . . . 8 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 dom dom 𝐻
29	28	nfcri 2891	. . . . . . 7 ⊢ Ⅎ𝑥 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
30	27, 29	nfan 1901	. . . . . 6 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
31		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
32	23, 24, 25, 26, 30, 31, 31	iinfssclem3 49546	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → (𝑎𝐾𝑎) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎))
33	22, 32	eleqtrrd 2840	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎))
34		simprl 771	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑓 ∈ (𝑎𝐾𝑏))
35	1	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝐴 ≠ ∅)
36	24	adantlr 716	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
37	5	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
38		eqidd 2738	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
39	28	nfcri 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
40	28	nfcri 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
41	39, 40	nfan 1901	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
42	30, 41	nfan 1901	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻))
43	31	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
44		simprl 771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
45	35, 36, 37, 38, 42, 43, 44	iinfssclem3 49546	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑎𝐾𝑏) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
46	45	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑎𝐾𝑏) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
47	34, 46	eleqtrd 2839	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
48		simprr 773	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑔 ∈ (𝑏𝐾𝑐))
49		simprr 773	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
50	35, 36, 37, 38, 42, 44, 49	iinfssclem3 49546	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑏𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
51	50	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑏𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
52	48, 51	eleqtrd 2839	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
53	47, 52	jca 511	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)))
54		nfii1 4972	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏)
55	54	nfcri 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏)
56		nfii1 4972	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)
57	56	nfcri 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)
58	55, 57	nfan 1901	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
59	42, 58	nfan 1901	. . . . . . . . . 10 ⊢ Ⅎ𝑥(((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)))
60	2	ad5ant15 759	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝐻 ∈ (Subcat‘𝐶))
61	9	ad5ant15 759	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
62		iinss2 5001	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻)
63	62	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻)
64	43	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
65	63, 64	sseldd 3923	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑎 ∈ dom dom 𝐻)
66		eqid 2737	. . . . . . . . . . 11 ⊢ (comp‘𝐶) = (comp‘𝐶)
67	44	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
68	63, 67	sseldd 3923	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ dom dom 𝐻)
69	49	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
70	63, 69	sseldd 3923	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑐 ∈ dom dom 𝐻)
71		iinss2 5001	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ⊆ (𝑎𝐻𝑏))
72	71	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ⊆ (𝑎𝐻𝑏))
73		simplrl 777	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
74	72, 73	sseldd 3923	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑓 ∈ (𝑎𝐻𝑏))
75		iinss2 5001	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐) ⊆ (𝑏𝐻𝑐))
76	75	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐) ⊆ (𝑏𝐻𝑐))
77		simplrr 778	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
78	76, 77	sseldd 3923	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ (𝑏𝐻𝑐))
79	60, 61, 65, 66, 68, 70, 74, 78	subccocl 17806	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
80	59, 79	ralrimia 3237	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) → ∀𝑥 ∈ 𝐴 (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
81		ovex 7394	. . . . . . . . . 10 ⊢ (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ V
82		eliin 4939	. . . . . . . . . 10 ⊢ ((𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ V → ((𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐) ↔ ∀𝑥 ∈ 𝐴 (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐)))
83	81, 82	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐) ↔ ∀𝑥 ∈ 𝐴 (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
84	80, 83	sylibr 234	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
85	53, 84	syldan 592	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
86	35, 36, 37, 38, 42, 43, 49	iinfssclem3 49546	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑎𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
87	86	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑎𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
88	85, 87	eleqtrrd 2840	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
89	88	ralrimivva 3181	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → ∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
90	89	ralrimivva 3181	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
91	33, 90	jca 511	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → (((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))
92	91	ralrimiva 3130	. 2 ⊢ (𝜑 → ∀𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻(((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))
93		n0 4294	. . . . 5 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
94	1, 93	sylib 218	. . . 4 ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
95		subcrcl 17777	. . . . 5 ⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat)
96	2, 95	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ Cat)
97	94, 96	exlimddv 1937	. . 3 ⊢ (𝜑 → 𝐶 ∈ Cat)
98	1, 4, 5, 8, 27	iinfssclem2 49545	. . 3 ⊢ (𝜑 → 𝐾 Fn (∩ 𝑥 ∈ 𝐴 dom dom 𝐻 × ∩ 𝑥 ∈ 𝐴 dom dom 𝐻))
99	3, 12, 66, 97, 98	issubc2 17797	. 2 ⊢ (𝜑 → (𝐾 ∈ (Subcat‘𝐶) ↔ (𝐾 ⊆_cat (Hom_f ‘𝐶) ∧ ∀𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻(((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))))
100	6, 92, 99	mpbir2and 714	1 ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 Vcvv 3430 ⊆ wss 3890 ∅c0 4274 ⟨cop 4574 ∩ ciin 4935 class class class wbr 5086 ↦ cmpt 5167 × cxp 5623 dom cdm 5625 Fn wfn 6488 ‘cfv 6493 (class class class)co 7361 compcco 17226 Catccat 17624 Idccid 17625 Hom_f chomf 17626 ⊆_cat cssc 17768 Subcatcsubc 17770

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-ov 7364 df-oprab 7365 df-mpo 7366 df-1st 7936 df-2nd 7937 df-pm 8770 df-ixp 8840 df-ssc 17771 df-subc 17773

This theorem is referenced by: infsubc 49550

W3C validator