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 50165

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 2761	. . . 4 ⊢ (Hom_f ‘𝐶) = (Hom_f ‘𝐶)
4	2, 3	subcssc 18015	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
5		iinfsubc.3	. . 3 ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
6	1, 4, 5	iinfssc 50164	. 2 ⊢ (𝜑 → 𝐾 ⊆_cat (Hom_f ‘𝐶))
7	2	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → 𝐻 ∈ (Subcat‘𝐶))
8		eqidd 2762	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
9	2, 8	subcfn 18016	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
10	9	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
11		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → 𝑎 ∈ dom dom 𝐻)
12		eqid 2761	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
13	7, 10, 11, 12	subcidcl 18019	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑎 ∈ dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎))
14	13	ex 418	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑎 ∈ dom dom 𝐻 → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
15	14	ralimdva 3175	. . . . . . 7 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻 → ∀𝑥 ∈ 𝐴 ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐻𝑎)))
16		eliin 4956	. . . . . . . 8 ⊢ (𝑎 ∈ V → (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻))
17	16	elv 3456	. . . . . . 7 ⊢ (𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻)
18		fvex 6898	. . . . . . . 8 ⊢ ((Id‘𝐶)‘𝑎) ∈ V
19		eliin 4956	. . . . . . . 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 412	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎))
23	1	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → 𝐴 ≠ ∅)
24	4	adantlr 728	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
25	5	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
26		eqidd 2762	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
27		nfv 1947	. . . . . . 7 ⊢ Ⅎ𝑥𝜑
28		nfii1 4987	. . . . . . . 8 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 dom dom 𝐻
29	28	nfcri 2915	. . . . . . 7 ⊢ Ⅎ𝑥 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
30	27, 29	nfan 1932	. . . . . 6 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
31		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
32	23, 24, 25, 26, 30, 31, 31	iinfssclem3 50163	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → (𝑎𝐾𝑎) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑎))
33	22, 32	eleqtrrd 2864	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → ((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎))
34		simprl 783	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑓 ∈ (𝑎𝐾𝑏))
35	1	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝐴 ≠ ∅)
36	24	adantlr 728	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆_cat (Hom_f ‘𝐶))
37	5	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦)))
38		eqidd 2762	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ 𝑥 ∈ 𝐴) → dom dom 𝐻 = dom dom 𝐻)
39	28	nfcri 2915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
40	28	nfcri 2915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
41	39, 40	nfan 1932	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
42	30, 41	nfan 1932	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻))
43	31	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
44		simprl 783	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
45	35, 36, 37, 38, 42, 43, 44	iinfssclem3 50163	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑎𝐾𝑏) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
46	45	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑎𝐾𝑏) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
47	34, 46	eleqtrd 2863	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
48		simprr 785	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑔 ∈ (𝑏𝐾𝑐))
49		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
50	35, 36, 37, 38, 42, 44, 49	iinfssclem3 50163	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑏𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
51	50	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑏𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
52	48, 51	eleqtrd 2863	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
53	47, 52	jca 521	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)))
54		nfii1 4987	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏)
55	54	nfcri 2915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏)
56		nfii1 4987	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)
57	56	nfcri 2915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)
58	55, 57	nfan 1932	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
59	42, 58	nfan 1932	. . . . . . . . . 10 ⊢ Ⅎ𝑥(((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐)))
60	2	ad5ant15 771	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝐻 ∈ (Subcat‘𝐶))
61	9	ad5ant15 771	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻))
62		iinss2 5016	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻)
63	62	adantl 487	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻)
64	43	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
65	63, 64	sseldd 3932	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑎 ∈ dom dom 𝐻)
66		eqid 2761	. . . . . . . . . . 11 ⊢ (comp‘𝐶) = (comp‘𝐶)
67	44	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
68	63, 67	sseldd 3932	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ dom dom 𝐻)
69	49	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)
70	63, 69	sseldd 3932	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑐 ∈ dom dom 𝐻)
71		iinss2 5016	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ⊆ (𝑎𝐻𝑏))
72	71	adantl 487	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ⊆ (𝑎𝐻𝑏))
73		simplrl 789	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏))
74	72, 73	sseldd 3932	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑓 ∈ (𝑎𝐻𝑏))
75		iinss2 5016	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐) ⊆ (𝑏𝐻𝑐))
76	75	adantl 487	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐) ⊆ (𝑏𝐻𝑐))
77		simplrr 790	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))
78	76, 77	sseldd 3932	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ (𝑏𝐻𝑐))
79	60, 61, 65, 66, 68, 70, 74, 78	subccocl 18020	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) ∧ 𝑥 ∈ 𝐴) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
80	59, 79	ralrimia 3262	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑏) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 (𝑏𝐻𝑐))) → ∀𝑥 ∈ 𝐴 (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐻𝑐))
81		ovex 7453	. . . . . . . . . 10 ⊢ (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ V
82		eliin 4956	. . . . . . . . . 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 603	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
86	35, 36, 37, 38, 42, 43, 49	iinfssclem3 50163	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → (𝑎𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
87	86	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑎𝐾𝑐) = ∩ 𝑥 ∈ 𝐴 (𝑎𝐻𝑐))
88	85, 87	eleqtrrd 2864	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) ∧ (𝑓 ∈ (𝑎𝐾𝑏) ∧ 𝑔 ∈ (𝑏𝐾𝑐))) → (𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
89	88	ralrimivva 3206	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) ∧ (𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻)) → ∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
90	89	ralrimivva 3206	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐))
91	33, 90	jca 521	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻) → (((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))
92	91	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻(((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))
93		n0 4300	. . . . 5 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
94	1, 93	sylib 221	. . . 4 ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
95		subcrcl 17991	. . . . 5 ⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat)
96	2, 95	syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ Cat)
97	94, 96	exlimddv 1968	. . 3 ⊢ (𝜑 → 𝐶 ∈ Cat)
98	1, 4, 5, 8, 27	iinfssclem2 50162	. . 3 ⊢ (𝜑 → 𝐾 Fn (∩ 𝑥 ∈ 𝐴 dom dom 𝐻 × ∩ 𝑥 ∈ 𝐴 dom dom 𝐻))
99	3, 12, 66, 97, 98	issubc2 18011	. 2 ⊢ (𝜑 → (𝐾 ∈ (Subcat‘𝐶) ↔ (𝐾 ⊆_cat (Hom_f ‘𝐶) ∧ ∀𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻(((Id‘𝐶)‘𝑎) ∈ (𝑎𝐾𝑎) ∧ ∀𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻∀𝑓 ∈ (𝑎𝐾𝑏)∀𝑔 ∈ (𝑏𝐾𝑐)(𝑔(⟨𝑎, 𝑏⟩(comp‘𝐶)𝑐)𝑓) ∈ (𝑎𝐾𝑐)))))
100	6, 92, 99	mpbir2and 726	1 ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐶))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 Vcvv 3451 ⊆ wss 3899 ∅c0 4279 ⟨cop 4590 ∩ ciin 4952 class class class wbr 5103 ↦ cmpt 5186 × cxp 5649 dom cdm 5651 Fn wfn 6533 ‘cfv 6538 (class class class)co 7420 compcco 17440 Catccat 17838 Idccid 17839 Hom_f chomf 17840 ⊆_cat cssc 17982 Subcatcsubc 17984

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7423 df-oprab 7424 df-mpo 7425 df-1st 8001 df-2nd 8002 df-pm 8850 df-ixp 8926 df-ssc 17985 df-subc 17987

This theorem is used by: infsubc 50167

W3C validator