Theorem fpwwe2lem1

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Hypothesis	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\}$$
Assertion	fpwwe2lem1	$$⊢W\subseteq 𝒫A\times 𝒫\left(A\times A\right)$$

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		simpll	$$⊢\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)\to x\subseteq A$$
3		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
4	2 3	sylibr	$$⊢\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)\to x\in 𝒫A$$
5		simplr	$$⊢\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)\to r\subseteq x\times x$$
6		xpss12	$$⊢\left(x\subseteq A\wedge x\subseteq A\right)\to x\times x\subseteq A\times A$$
7	2 2 6	syl2anc	$$⊢\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)\to x\times x\subseteq A\times A$$
8	5 7	sstrd	$$⊢\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)\to r\subseteq A\times A$$
9		velpw	$$⊢r\in 𝒫\left(A\times A\right)\leftrightarrow r\subseteq A\times A$$
10	8 9	sylibr	$$⊢\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)\to r\in 𝒫\left(A\times A\right)$$
11	4 10	jca	$$⊢\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)\to \left(x\in 𝒫A\wedge r\in 𝒫\left(A\times A\right)\right)$$
12	11	ssopab2i	$$⊢\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\}\subseteq \left\{⟨x,r⟩|\left(x\in 𝒫A\wedge r\in 𝒫\left(A\times A\right)\right)\right\}$$
13		df-xp	$$⊢𝒫A\times 𝒫\left(A\times A\right)=\left\{⟨x,r⟩|\left(x\in 𝒫A\wedge r\in 𝒫\left(A\times A\right)\right)\right\}$$
14	12 1 13	3sstr4i	$$⊢W\subseteq 𝒫A\times 𝒫\left(A\times A\right)$$