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 49720

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 2769	. . . 4 ⊢ (Hom_f ‘𝐶) = (Hom_f ‘𝐶)
4	2, 3	subcssc 17896	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
5		iinfsubc.3	. . 3 ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
6	1, 4, 5	iinfssc 49719	. 2 ⊢ (𝜑 → 𝐾 ⊆_cat (Hom_f ‘𝐶))
7	2	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → 𝐻 ∈ (Subcat‘𝐶))
8		eqidd 2770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
9	2, 8	subcfn 17897	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
10	9	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
11		simpr 489	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → 𝑎 ∈ dom dom 𝐻)
12		eqid 2769	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
13	7, 10, 11, 12	subcidcl 17900	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎))
14	13	ex 417	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑎 ∈ dom dom 𝐻 → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
15	14	ralimdva 3183	. . . . . . 7 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻 → ∀𝑥 ∈ 𝐴 ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
16		eliin 4965	. . . . . . . 8 ⊢ (𝑎 ∈ V → (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻))
17	16	elv 3468	. . . . . . 7 ⊢ (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻)
18		fvex 6895	. . . . . . . 8 ⊢ ((Id‘𝐶)‘𝑎) ∈ V
19		eliin 4965	. . . . . . . 8 ⊢ (((Id‘𝐶)‘𝑎) ∈ V → (((Id‘𝐶)‘𝑎) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎) ↔ ∀𝑥 ∈ 𝐴 ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
20	18, 19	ax-mp 5	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑎) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎) ↔ ∀𝑥 ∈ 𝐴 ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎))
21	15, 17, 20	3imtr4g 299	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 → ((Id‘𝐶)‘𝑎) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎)))
22	21	imp 411	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎))
23	1	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → 𝐴 ≠ ∅)
24	4	adantlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
25	5	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
26		eqidd 2770	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
27		nfv 1941	. . . . . . 7 ⊢ Ⅎ𝑥𝜑
28		nfii1 4997	. . . . . . . 8 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 dom dom 𝐻
29	28	nfcri 2923	. . . . . . 7 ⊢ Ⅎ𝑥 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
30	27, 29	nfan 1926	. . . . . 6 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
31		simpr 489	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
32	23, 24, 25, 26, 30, 31, 31	iinfssclem3 49718	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → (𝑎𝐾𝑎) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎))
33	22, 32	eleqtrrd 2872	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎))
34		simprl 782	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑓 ∈ (𝑎𝐾𝑏))
35	1	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝐴 ≠ ∅)
36	24	adantlr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
37	5	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
38		eqidd 2770	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
39	28	nfcri 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
40	28	nfcri 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
41	39, 40	nfan 1926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
42	30, 41	nfan 1926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻))
43	31	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
44		simprl 782	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
45	35, 36, 37, 38, 42, 43, 44	iinfssclem3 49718	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑎𝐾𝑏) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
46	45	adantr 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑎𝐾𝑏) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
47	34, 46	eleqtrd 2871	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
48		simprr 784	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑔 ∈ (𝑏𝐾𝑐))
49		simprr 784	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
50	35, 36, 37, 38, 42, 44, 49	iinfssclem3 49718	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑏𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
51	50	adantr 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑏𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
52	48, 51	eleqtrd 2871	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
53	47, 52	jca 520	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)))
54		nfii1 4997	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏)
55	54	nfcri 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏)
56		nfii1 4997	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)
57	56	nfcri 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)
58	55, 57	nfan 1926	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
59	42, 58	nfan 1926	. . . . . . . . . 10 ⊢ Ⅎ𝑥(((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)))
60	2	ad5ant15 770	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝐻 ∈ (Subcat‘𝐶))
61	9	ad5ant15 770	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
62		iinss2 5026	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻)
63	62	adantl 486	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻)
64	43	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
65	63, 64	sseldd 3946	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑎 ∈ dom dom 𝐻)
66		eqid 2769	. . . . . . . . . . 11 ⊢ (comp‘𝐶) = (comp‘𝐶)
67	44	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
68	63, 67	sseldd 3946	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ dom dom 𝐻)
69	49	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
70	63, 69	sseldd 3946	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑐 ∈ dom dom 𝐻)
71		iinss2 5026	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ⊆ (𝑎𝐻𝑏))
72	71	adantl 486	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ⊆ (𝑎𝐻𝑏))
73		simplrl 788	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
74	72, 73	sseldd 3946	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑓 ∈ (𝑎𝐻𝑏))
75		iinss2 5026	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐) ⊆ (𝑏𝐻𝑐))
76	75	adantl 486	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐) ⊆ (𝑏𝐻𝑐))
77		simplrr 789	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
78	76, 77	sseldd 3946	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ (𝑏𝐻𝑐))
79	60, 61, 65, 66, 68, 70, 74, 78	subccocl 17901	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
80	59, 79	ralrimia 3270	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) → ∀𝑥 ∈ 𝐴 (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
81		ovex 7444	. . . . . . . . . 10 ⊢ (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ V
82		eliin 4965	. . . . . . . . . 10 ⊢ ((𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ V → ((𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐) ↔ ∀𝑥 ∈ 𝐴 (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐)))
83	81, 82	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐) ↔ ∀𝑥 ∈ 𝐴 (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
84	80, 83	sylibr 237	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
85	53, 84	syldan 602	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
86	35, 36, 37, 38, 42, 43, 49	iinfssclem3 49718	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑎𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
87	86	adantr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑎𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
88	85, 87	eleqtrrd 2872	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
89	88	ralrimivva 3214	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → ∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
90	89	ralrimivva 3214	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
91	33, 90	jca 520	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → (((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))
92	91	ralrimiva 3163	. 2 ⊢ (𝜑 → ∀𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻(((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))
93		n0 4315	. . . . 5 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
94	1, 93	sylib 221	. . . 4 ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
95		subcrcl 17872	. . . . 5 ⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat)
96	2, 95	syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ Cat)
97	94, 96	exlimddv 1962	. . 3 ⊢ (𝜑 → 𝐶 ∈ Cat)
98	1, 4, 5, 8, 27	iinfssclem2 49717	. . 3 ⊢ (𝜑 → 𝐾 Fn (∩ 𝑥 ∈ 𝐴 dom dom 𝐻 × ∩ 𝑥 ∈ 𝐴 dom dom 𝐻))
99	3, 12, 66, 97, 98	issubc2 17892	. 2 ⊢ (𝜑 → (𝐾 ∈ (Subcat‘𝐶) ↔ (𝐾 ⊆_cat (Hom_f ‘𝐶) ∧ ∀𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻(((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))))
100	6, 92, 99	mpbir2and 725	1 ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ∃wex 1806 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 Vcvv 3463 ⊆ wss 3913 ∅c0 4294 ⟨cop 4600 ∩ ciin 4961 class class class wbr 5113 ↦ cmpt 5196 × cxp 5660 dom cdm 5662 Fn wfn 6532 ‘cfv 6537 (class class class)co 7411 compcco 17321 Catccat 17719 Idccid 17720 Hom_f chomf 17721 ⊆_cat cssc 17863 Subcatcsubc 17865

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-iin 4963 df-br 5114 df-opab 5178 df-mpt 5197 df-id 5557 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-ov 7414 df-oprab 7415 df-mpo 7416 df-1st 7985 df-2nd 7986 df-pm 8826 df-ixp 8895 df-ssc 17866 df-subc 17868

This theorem is referenced by: infsubc 49722

W3C validator