Theorem fpwwe2lem3

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 19-May-2015) (Revised by AV, 20-Jul-2024)

	Ref	Expression
Hypotheses	fpwwe2.1	$$⊢W=\left\{⟨x,r⟩|\left(\left(x\subseteq A\wedge r\subseteq x\times x\right)\wedge \left(r\mathrm{We}x\wedge \forall y\in x\underset{\dot{}}{[}{r}^{-1}\left[\left\{y\right\}\right]/u\underset{\dot{}}{]}uF\left(r\cap \left(u\times u\right)\right)=y\right)\right)\right\}$$
	fpwwe2.2	$$⊢\phi \to A\in V$$
	fpwwe2lem3.4	$$⊢\phi \to XWR$$
Assertion	fpwwe2lem3	$$⊢\left(\phi \wedge B\in X\right)\to R^{-1}\left[\left\{B\right\}\right]F\left(R\cap \left(R^{-1}\left[\left\{B\right\}\right]\times R^{-1}\left[\left\{B\right\}\right]\right)\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		fpwwe2.1	$$⊢W=\left\{⟨x,r⟩|\left(\left(x\subseteq A\wedge r\subseteq x\times x\right)\wedge \left(r\mathrm{We}x\wedge \forall y\in x\underset{\dot{}}{[}{r}^{-1}\left[\left\{y\right\}\right]/u\underset{\dot{}}{]}uF\left(r\cap \left(u\times u\right)\right)=y\right)\right)\right\}$$
2		fpwwe2.2	$$⊢\phi \to A\in V$$
3		fpwwe2lem3.4	$$⊢\phi \to XWR$$
4	1 2	fpwwe2lem2	$$⊢\phi \to \left(XWR\leftrightarrow \left(\left(X\subseteq A\wedge R\subseteq X\times X\right)\wedge \left(R\mathrm{We}X\wedge \forall y\in X\underset{\dot{}}{[}{R}^{-1}\left[\left\{y\right\}\right]/u\underset{\dot{}}{]}uF\left(R\cap \left(u\times u\right)\right)=y\right)\right)\right)$$
5	3 4	mpbid	$$⊢\phi \to \left(\left(X\subseteq A\wedge R\subseteq X\times X\right)\wedge \left(R\mathrm{We}X\wedge \forall y\in X\underset{\dot{}}{[}{R}^{-1}\left[\left\{y\right\}\right]/u\underset{\dot{}}{]}uF\left(R\cap \left(u\times u\right)\right)=y\right)\right)$$
6	5	simprrd	$$⊢\phi \to \forall y\in X\underset{\dot{}}{[}{R}^{-1}\left[\left\{y\right\}\right]/u\underset{\dot{}}{]}uF\left(R\cap \left(u\times u\right)\right)=y$$
7		sneq	$$⊢y=B\to \left\{y\right\}=\left\{B\right\}$$
8	7	imaeq2d	$$⊢y=B\to R^{-1}\left[\left\{y\right\}\right]=R^{-1}\left[\left\{B\right\}\right]$$
9		eqeq2	$$⊢y=B\to \left(uF\left(R\cap \left(u\times u\right)\right)=y\leftrightarrow uF\left(R\cap \left(u\times u\right)\right)=B\right)$$
10	8 9	sbceqbid	$$⊢y=B\to \left(\underset{\dot{}}{[}{R}^{-1}\left[\left\{y\right\}\right]/u\underset{\dot{}}{]}uF\left(R\cap \left(u\times u\right)\right)=y\leftrightarrow \underset{\dot{}}{[}{R}^{-1}\left[\left\{B\right\}\right]/u\underset{\dot{}}{]}uF\left(R\cap \left(u\times u\right)\right)=B\right)$$
11	10	rspccva	$$⊢\left(\forall y\in X\underset{\dot{}}{[}{R}^{-1}\left[\left\{y\right\}\right]/u\underset{\dot{}}{]}uF\left(R\cap \left(u\times u\right)\right)=y\wedge B\in X\right)\to \underset{\dot{}}{[}{R}^{-1}\left[\left\{B\right\}\right]/u\underset{\dot{}}{]}uF\left(R\cap \left(u\times u\right)\right)=B$$
12	6 11	sylan	$$⊢\left(\phi \wedge B\in X\right)\to \underset{\dot{}}{[}{R}^{-1}\left[\left\{B\right\}\right]/u\underset{\dot{}}{]}uF\left(R\cap \left(u\times u\right)\right)=B$$
13		cnvimass	$$⊢R^{-1}\left[\left\{B\right\}\right]\subseteq \mathrm{dom}R$$
14	1	relopabiv	$$⊢\mathrm{Rel}W$$
15	14	brrelex2i	$$⊢XWR\to R\in \mathrm{V}$$
16		dmexg	$$⊢R\in \mathrm{V}\to \mathrm{dom}R\in \mathrm{V}$$
17	3 15 16	3syl	$$⊢\phi \to \mathrm{dom}R\in \mathrm{V}$$
18		ssexg	$$⊢\left(R^{-1}\left[\left\{B\right\}\right]\subseteq \mathrm{dom}R\wedge \mathrm{dom}R\in \mathrm{V}\right)\to R^{-1}\left[\left\{B\right\}\right]\in \mathrm{V}$$
19	13 17 18	sylancr	$$⊢\phi \to R^{-1}\left[\left\{B\right\}\right]\in \mathrm{V}$$
20		id	$$⊢u=R^{-1}\left[\left\{B\right\}\right]\to u=R^{-1}\left[\left\{B\right\}\right]$$
21	20	sqxpeqd	$$⊢u=R^{-1}\left[\left\{B\right\}\right]\to u\times u=R^{-1}\left[\left\{B\right\}\right]\times R^{-1}\left[\left\{B\right\}\right]$$
22	21	ineq2d	$$⊢u=R^{-1}\left[\left\{B\right\}\right]\to R\cap \left(u\times u\right)=R\cap \left(R^{-1}\left[\left\{B\right\}\right]\times R^{-1}\left[\left\{B\right\}\right]\right)$$
23	20 22	oveq12d	$$⊢u=R^{-1}\left[\left\{B\right\}\right]\to uF\left(R\cap \left(u\times u\right)\right)=R^{-1}\left[\left\{B\right\}\right]F\left(R\cap \left(R^{-1}\left[\left\{B\right\}\right]\times R^{-1}\left[\left\{B\right\}\right]\right)\right)$$
24	23	eqeq1d	$$⊢u=R^{-1}\left[\left\{B\right\}\right]\to \left(uF\left(R\cap \left(u\times u\right)\right)=B\leftrightarrow R^{-1}\left[\left\{B\right\}\right]F\left(R\cap \left(R^{-1}\left[\left\{B\right\}\right]\times R^{-1}\left[\left\{B\right\}\right]\right)\right)=B\right)$$
25	24	sbcieg	$$⊢R^{-1}\left[\left\{B\right\}\right]\in \mathrm{V}\to \left(\underset{\dot{}}{[}{R}^{-1}\left[\left\{B\right\}\right]/u\underset{\dot{}}{]}uF\left(R\cap \left(u\times u\right)\right)=B\leftrightarrow R^{-1}\left[\left\{B\right\}\right]F\left(R\cap \left(R^{-1}\left[\left\{B\right\}\right]\times R^{-1}\left[\left\{B\right\}\right]\right)\right)=B\right)$$
26	19 25	syl	$$⊢\phi \to \left(\underset{\dot{}}{[}{R}^{-1}\left[\left\{B\right\}\right]/u\underset{\dot{}}{]}uF\left(R\cap \left(u\times u\right)\right)=B\leftrightarrow R^{-1}\left[\left\{B\right\}\right]F\left(R\cap \left(R^{-1}\left[\left\{B\right\}\right]\times R^{-1}\left[\left\{B\right\}\right]\right)\right)=B\right)$$
27	26	adantr	$$⊢\left(\phi \wedge B\in X\right)\to \left(\underset{\dot{}}{[}{R}^{-1}\left[\left\{B\right\}\right]/u\underset{\dot{}}{]}uF\left(R\cap \left(u\times u\right)\right)=B\leftrightarrow R^{-1}\left[\left\{B\right\}\right]F\left(R\cap \left(R^{-1}\left[\left\{B\right\}\right]\times R^{-1}\left[\left\{B\right\}\right]\right)\right)=B\right)$$
28	12 27	mpbid	$$⊢\left(\phi \wedge B\in X\right)\to R^{-1}\left[\left\{B\right\}\right]F\left(R\cap \left(R^{-1}\left[\left\{B\right\}\right]\times R^{-1}\left[\left\{B\right\}\right]\right)\right)=B$$