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 48931

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 2734	. . . 4 ⊢ (Hom_f ‘𝐶) = (Hom_f ‘𝐶)
4	2, 3	subcssc 17857	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
5		iinfsubc.3	. . 3 ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
6	1, 4, 5	iinfssc 48930	. 2 ⊢ (𝜑 → 𝐾 ⊆_cat (Hom_f ‘𝐶))
7	2	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → 𝐻 ∈ (Subcat‘𝐶))
8		eqidd 2735	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
9	2, 8	subcfn 17858	. . . . . . . . . . 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 2734	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
13	7, 10, 11, 12	subcidcl 17861	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎))
14	13	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑎 ∈ dom dom 𝐻 → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
15	14	ralimdva 3154	. . . . . . 7 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻 → ∀𝑥 ∈ 𝐴 ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
16		eliin 4976	. . . . . . . 8 ⊢ (𝑎 ∈ V → (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻))
17	16	elv 3468	. . . . . . 7 ⊢ (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻)
18		fvex 6899	. . . . . . . 8 ⊢ ((Id‘𝐶)‘𝑎) ∈ V
19		eliin 4976	. . . . . . . 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 715	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
25	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
26		eqidd 2735	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
27		nfv 1913	. . . . . . 7 ⊢ Ⅎ𝑥𝜑
28		nfii1 5009	. . . . . . . 8 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 dom dom 𝐻
29	28	nfcri 2889	. . . . . . 7 ⊢ Ⅎ𝑥 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
30	27, 29	nfan 1898	. . . . . 6 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
31		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
32	23, 24, 25, 26, 30, 31, 31	iinfssclem3 48929	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → (𝑎𝐾𝑎) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎))
33	22, 32	eleqtrrd 2836	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎))
34		simprl 770	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑓 ∈ (𝑎𝐾𝑏))
35	1	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝐴 ≠ ∅)
36	24	adantlr 715	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
37	5	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
38		eqidd 2735	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
39	28	nfcri 2889	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
40	28	nfcri 2889	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
41	39, 40	nfan 1898	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
42	30, 41	nfan 1898	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻))
43	31	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
44		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
45	35, 36, 37, 38, 42, 43, 44	iinfssclem3 48929	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑎𝐾𝑏) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
46	45	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑎𝐾𝑏) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
47	34, 46	eleqtrd 2835	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
48		simprr 772	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑔 ∈ (𝑏𝐾𝑐))
49		simprr 772	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
50	35, 36, 37, 38, 42, 44, 49	iinfssclem3 48929	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑏𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
51	50	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑏𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
52	48, 51	eleqtrd 2835	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
53	47, 52	jca 511	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)))
54		nfii1 5009	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏)
55	54	nfcri 2889	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏)
56		nfii1 5009	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)
57	56	nfcri 2889	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)
58	55, 57	nfan 1898	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
59	42, 58	nfan 1898	. . . . . . . . . 10 ⊢ Ⅎ𝑥(((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)))
60	2	ad5ant15 758	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝐻 ∈ (Subcat‘𝐶))
61	9	ad5ant15 758	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
62		iinss2 5037	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻)
63	62	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻)
64	43	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
65	63, 64	sseldd 3964	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑎 ∈ dom dom 𝐻)
66		eqid 2734	. . . . . . . . . . 11 ⊢ (comp‘𝐶) = (comp‘𝐶)
67	44	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
68	63, 67	sseldd 3964	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ dom dom 𝐻)
69	49	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
70	63, 69	sseldd 3964	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑐 ∈ dom dom 𝐻)
71		iinss2 5037	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ⊆ (𝑎𝐻𝑏))
72	71	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ⊆ (𝑎𝐻𝑏))
73		simplrl 776	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
74	72, 73	sseldd 3964	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑓 ∈ (𝑎𝐻𝑏))
75		iinss2 5037	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐) ⊆ (𝑏𝐻𝑐))
76	75	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐) ⊆ (𝑏𝐻𝑐))
77		simplrr 777	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
78	76, 77	sseldd 3964	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ (𝑏𝐻𝑐))
79	60, 61, 65, 66, 68, 70, 74, 78	subccocl 17862	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
80	59, 79	ralrimia 3244	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) → ∀𝑥 ∈ 𝐴 (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
81		ovex 7446	. . . . . . . . . 10 ⊢ (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ V
82		eliin 4976	. . . . . . . . . 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 591	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
86	35, 36, 37, 38, 42, 43, 49	iinfssclem3 48929	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑎𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
87	86	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑎𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
88	85, 87	eleqtrrd 2836	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
89	88	ralrimivva 3189	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → ∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
90	89	ralrimivva 3189	. . . 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 3133	. 2 ⊢ (𝜑 → ∀𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻(((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))
93		n0 4333	. . . . 5 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
94	1, 93	sylib 218	. . . 4 ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
95		subcrcl 17832	. . . . 5 ⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat)
96	2, 95	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ Cat)
97	94, 96	exlimddv 1934	. . 3 ⊢ (𝜑 → 𝐶 ∈ Cat)
98	1, 4, 5, 8, 27	iinfssclem2 48928	. . 3 ⊢ (𝜑 → 𝐾 Fn (∩ 𝑥 ∈ 𝐴 dom dom 𝐻 × ∩ 𝑥 ∈ 𝐴 dom dom 𝐻))
99	3, 12, 66, 97, 98	issubc2 17853	. 2 ⊢ (𝜑 → (𝐾 ∈ (Subcat‘𝐶) ↔ (𝐾 ⊆_cat (Hom_f ‘𝐶) ∧ ∀𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻(((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))))
100	6, 92, 99	mpbir2and 713	1 ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ∃wex 1778 ∈ wcel 2107 ≠ wne 2931 ∀wral 3050 Vcvv 3463 ⊆ wss 3931 ∅c0 4313 ⟨cop 4612 ∩ ciin 4972 class class class wbr 5123 ↦ cmpt 5205 × cxp 5663 dom cdm 5665 Fn wfn 6536 ‘cfv 6541 (class class class)co 7413 compcco 17286 Catccat 17679 Idccid 17680 Hom_f chomf 17681 ⊆_cat cssc 17823 Subcatcsubc 17825

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-ral 3051 df-rex 3060 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-iin 4974 df-br 5124 df-opab 5186 df-mpt 5206 df-id 5558 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-ov 7416 df-oprab 7417 df-mpo 7418 df-1st 7996 df-2nd 7997 df-pm 8851 df-ixp 8920 df-ssc 17826 df-subc 17828

This theorem is referenced by: infsubc 48933

W3C validator