Theorem sscid

Description: The subcategory subset relation is reflexive. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Assertion	sscid	$$⊢\left(HFn\left(S\times S\right)\wedge S\in V\right)\to H{\subseteq }_{\mathrm{cat}}H$$

Proof

Step	Hyp	Ref	Expression
1		fnresdm	$$⊢HFn\left(S\times S\right)\to {H\upharpoonright }_{\left(S\times S\right)}=H$$
2	1	adantr	$$⊢\left(HFn\left(S\times S\right)\wedge S\in V\right)\to {H\upharpoonright }_{\left(S\times S\right)}=H$$
3		sscres	$$⊢\left(HFn\left(S\times S\right)\wedge S\in V\right)\to \left({H\upharpoonright }_{\left(S\times S\right)}\right){\subseteq }_{\mathrm{cat}}H$$
4	2 3	eqbrtrrd	$$⊢\left(HFn\left(S\times S\right)\wedge S\in V\right)\to H{\subseteq }_{\mathrm{cat}}H$$