Theorem catprsc2

Description: An alternate construction of the preorder induced by a category. See catprs2 for details. See also catprsc for a different construction. The two constructions are different because df-cat does not require the domain of H to be B X. B . (Contributed by Zhi Wang, 23-Sep-2024)

	Ref	Expression
Hypothesis	catprsc2.1	$$⊢\phi \to \underset{\dot{}}{\le }=\left\{⟨x,y⟩|xHy\ne \varnothing \right\}$$
Assertion	catprsc2	$$⊢\phi \to \forall z\in B\forall w\in B\left(z\underset{\dot{}}{\le }w\leftrightarrow zHw\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		catprsc2.1	$$⊢\phi \to \underset{\dot{}}{\le }=\left\{⟨x,y⟩|xHy\ne \varnothing \right\}$$
2	1	breqd	$$⊢\phi \to \left(z\underset{\dot{}}{\le }w\leftrightarrow z\left\{⟨x,y⟩|xHy\ne \varnothing \right\}w\right)$$
3		vex	$$⊢z\in \mathrm{V}$$
4		vex	$$⊢w\in \mathrm{V}$$
5		oveq12	$$⊢\left(x=z\wedge y=w\right)\to xHy=zHw$$
6	5	neeq1d	$$⊢\left(x=z\wedge y=w\right)\to \left(xHy\ne \varnothing \leftrightarrow zHw\ne \varnothing \right)$$
7		eqid	$$⊢\left\{⟨x,y⟩|xHy\ne \varnothing \right\}=\left\{⟨x,y⟩|xHy\ne \varnothing \right\}$$
8	3 4 6 7	braba	$$⊢z\left\{⟨x,y⟩|xHy\ne \varnothing \right\}w\leftrightarrow zHw\ne \varnothing$$
9	2 8	bitrdi	$$⊢\phi \to \left(z\underset{\dot{}}{\le }w\leftrightarrow zHw\ne \varnothing \right)$$
10	9	adantr	$$⊢\left(\phi \wedge \left(z\in B\wedge w\in B\right)\right)\to \left(z\underset{\dot{}}{\le }w\leftrightarrow zHw\ne \varnothing \right)$$
11	10	ralrimivva	$$⊢\phi \to \forall z\in B\forall w\in B\left(z\underset{\dot{}}{\le }w\leftrightarrow zHw\ne \varnothing \right)$$