Theorem xphe

Description: Any Cartesian product is hereditary in its second class. (Contributed by RP, 27-Mar-2020) (Proof shortened by OpenAI, 3-Jul-2020)

	Ref	Expression
Assertion	xphe	$$⊢\left(A\times B\right)hereditaryB$$

Proof

Step	Hyp	Ref	Expression
1		imassrn	$$⊢\left(A\times B\right)\left[B\right]\subseteq \mathrm{ran}\left(A\times B\right)$$
2		rnxpss	$$⊢\mathrm{ran}\left(A\times B\right)\subseteq B$$
3	1 2	sstri	$$⊢\left(A\times B\right)\left[B\right]\subseteq B$$
4		df-he	$$⊢\left(A\times B\right)hereditaryB\leftrightarrow \left(A\times B\right)\left[B\right]\subseteq B$$
5	3 4	mpbir	$$⊢\left(A\times B\right)hereditaryB$$