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 49533

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 2736	. . . 4 ⊢ (Hom_f ‘𝐶) = (Hom_f ‘𝐶)
4	2, 3	subcssc 17807	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
5		iinfsubc.3	. . 3 ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
6	1, 4, 5	iinfssc 49532	. 2 ⊢ (𝜑 → 𝐾 ⊆_cat (Hom_f ‘𝐶))
7	2	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → 𝐻 ∈ (Subcat‘𝐶))
8		eqidd 2737	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
9	2, 8	subcfn 17808	. . . . . . . . . . 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 2736	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
13	7, 10, 11, 12	subcidcl 17811	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎))
14	13	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑎 ∈ dom dom 𝐻 → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
15	14	ralimdva 3149	. . . . . . 7 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻 → ∀𝑥 ∈ 𝐴 ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
16		eliin 4938	. . . . . . . 8 ⊢ (𝑎 ∈ V → (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻))
17	16	elv 3434	. . . . . . 7 ⊢ (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻)
18		fvex 6853	. . . . . . . 8 ⊢ ((Id‘𝐶)‘𝑎) ∈ V
19		eliin 4938	. . . . . . . 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 2737	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
27		nfv 1916	. . . . . . 7 ⊢ Ⅎ𝑥𝜑
28		nfii1 4971	. . . . . . . 8 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 dom dom 𝐻
29	28	nfcri 2890	. . . . . . 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 49531	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → (𝑎𝐾𝑎) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎))
33	22, 32	eleqtrrd 2839	. . . 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 2737	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
39	28	nfcri 2890	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
40	28	nfcri 2890	. . . . . . . . . . . . . 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 49531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑎𝐾𝑏) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
46	45	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑎𝐾𝑏) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
47	34, 46	eleqtrd 2838	. . . . . . . . 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 49531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑏𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
51	50	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑏𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
52	48, 51	eleqtrd 2838	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
53	47, 52	jca 511	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)))
54		nfii1 4971	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏)
55	54	nfcri 2890	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏)
56		nfii1 4971	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)
57	56	nfcri 2890	. . . . . . . . . . . 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 5000	. . . . . . . . . . . . 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 3922	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑎 ∈ dom dom 𝐻)
66		eqid 2736	. . . . . . . . . . 11 ⊢ (comp‘𝐶) = (comp‘𝐶)
67	44	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
68	63, 67	sseldd 3922	. . . . . . . . . . 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 3922	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑐 ∈ dom dom 𝐻)
71		iinss2 5000	. . . . . . . . . . . . 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 3922	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑓 ∈ (𝑎𝐻𝑏))
75		iinss2 5000	. . . . . . . . . . . . 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 3922	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ (𝑏𝐻𝑐))
79	60, 61, 65, 66, 68, 70, 74, 78	subccocl 17812	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
80	59, 79	ralrimia 3236	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) → ∀𝑥 ∈ 𝐴 (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
81		ovex 7400	. . . . . . . . . 10 ⊢ (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ V
82		eliin 4938	. . . . . . . . . 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 49531	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑎𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
87	86	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑎𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
88	85, 87	eleqtrrd 2839	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
89	88	ralrimivva 3180	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → ∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
90	89	ralrimivva 3180	. . . 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 3129	. 2 ⊢ (𝜑 → ∀𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻(((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))
93		n0 4293	. . . . 5 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
94	1, 93	sylib 218	. . . 4 ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
95		subcrcl 17783	. . . . 5 ⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat)
96	2, 95	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ Cat)
97	94, 96	exlimddv 1937	. . 3 ⊢ (𝜑 → 𝐶 ∈ Cat)
98	1, 4, 5, 8, 27	iinfssclem2 49530	. . 3 ⊢ (𝜑 → 𝐾 Fn (∩ 𝑥 ∈ 𝐴 dom dom 𝐻 × ∩ 𝑥 ∈ 𝐴 dom dom 𝐻))
99	3, 12, 66, 97, 98	issubc2 17803	. 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 2932 ∀wral 3051 Vcvv 3429 ⊆ wss 3889 ∅c0 4273 ⟨cop 4573 ∩ ciin 4934 class class class wbr 5085 ↦ cmpt 5166 × cxp 5629 dom cdm 5631 Fn wfn 6493 ‘cfv 6498 (class class class)co 7367 compcco 17232 Catccat 17630 Idccid 17631 Hom_f chomf 17632 ⊆_cat cssc 17774 Subcatcsubc 17776

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 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689

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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3062 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-iin 4936 df-br 5086 df-opab 5148 df-mpt 5167 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-ov 7370 df-oprab 7371 df-mpo 7372 df-1st 7942 df-2nd 7943 df-pm 8776 df-ixp 8846 df-ssc 17777 df-subc 17779

This theorem is referenced by: infsubc 49535

W3C validator