Theorem catprslem

Description: Lemma for catprs . (Contributed by Zhi Wang, 18-Sep-2024)

	Ref	Expression
Hypotheses	catprs.1	$$⊢\phi \to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow xHy\ne \varnothing \right)$$
	catprslem.x	$$⊢\phi \to X\in B$$
	catprslem.y	$$⊢\phi \to Y\in B$$
Assertion	catprslem	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow XHY\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		catprs.1	$$⊢\phi \to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow xHy\ne \varnothing \right)$$
2		catprslem.x	$$⊢\phi \to X\in B$$
3		catprslem.y	$$⊢\phi \to Y\in B$$
4		breq1	$$⊢x=z\to \left(x\underset{\dot{}}{\le }y\leftrightarrow z\underset{\dot{}}{\le }y\right)$$
5		oveq1	$$⊢x=z\to xHy=zHy$$
6	5	neeq1d	$$⊢x=z\to \left(xHy\ne \varnothing \leftrightarrow zHy\ne \varnothing \right)$$
7	4 6	bibi12d	$$⊢x=z\to \left(\left(x\underset{\dot{}}{\le }y\leftrightarrow xHy\ne \varnothing \right)\leftrightarrow \left(z\underset{\dot{}}{\le }y\leftrightarrow zHy\ne \varnothing \right)\right)$$
8		breq2	$$⊢y=w\to \left(z\underset{\dot{}}{\le }y\leftrightarrow z\underset{\dot{}}{\le }w\right)$$
9		oveq2	$$⊢y=w\to zHy=zHw$$
10	9	neeq1d	$$⊢y=w\to \left(zHy\ne \varnothing \leftrightarrow zHw\ne \varnothing \right)$$
11	8 10	bibi12d	$$⊢y=w\to \left(\left(z\underset{\dot{}}{\le }y\leftrightarrow zHy\ne \varnothing \right)\leftrightarrow \left(z\underset{\dot{}}{\le }w\leftrightarrow zHw\ne \varnothing \right)\right)$$
12	7 11	cbvral2vw	$$⊢\forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow xHy\ne \varnothing \right)\leftrightarrow \forall z\in B\forall w\in B\left(z\underset{\dot{}}{\le }w\leftrightarrow zHw\ne \varnothing \right)$$
13	1 12	sylib	$$⊢\phi \to \forall z\in B\forall w\in B\left(z\underset{\dot{}}{\le }w\leftrightarrow zHw\ne \varnothing \right)$$
14		breq12	$$⊢\left(z=X\wedge w=Y\right)\to \left(z\underset{\dot{}}{\le }w\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
15		oveq12	$$⊢\left(z=X\wedge w=Y\right)\to zHw=XHY$$
16	15	neeq1d	$$⊢\left(z=X\wedge w=Y\right)\to \left(zHw\ne \varnothing \leftrightarrow XHY\ne \varnothing \right)$$
17	14 16	bibi12d	$$⊢\left(z=X\wedge w=Y\right)\to \left(\left(z\underset{\dot{}}{\le }w\leftrightarrow zHw\ne \varnothing \right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\leftrightarrow XHY\ne \varnothing \right)\right)$$
18	17	rspc2gv	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall z\in B\forall w\in B\left(z\underset{\dot{}}{\le }w\leftrightarrow zHw\ne \varnothing \right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow XHY\ne \varnothing \right)\right)$$
19	2 3 18	syl2anc	$$⊢\phi \to \left(\forall z\in B\forall w\in B\left(z\underset{\dot{}}{\le }w\leftrightarrow zHw\ne \varnothing \right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow XHY\ne \varnothing \right)\right)$$
20	13 19	mpd	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow XHY\ne \varnothing \right)$$