# Metamath Proof Explorer

## Theorem fpwwelem

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

Ref Expression
Hypotheses fpwwe.1 ${⊢}{W}=\left\{⟨{x},{r}⟩|\left(\left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\right)\wedge \left({r}\mathrm{We}{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{F}\left({{r}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right\}$
fpwwe.2 ${⊢}{\phi }\to {A}\in \mathrm{V}$
Assertion fpwwelem ${⊢}{\phi }\to \left({X}{W}{R}↔\left(\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\wedge \left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 fpwwe.1 ${⊢}{W}=\left\{⟨{x},{r}⟩|\left(\left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\right)\wedge \left({r}\mathrm{We}{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{F}\left({{r}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right\}$
2 fpwwe.2 ${⊢}{\phi }\to {A}\in \mathrm{V}$
3 1 relopabi ${⊢}\mathrm{Rel}{W}$
4 3 a1i ${⊢}{\phi }\to \mathrm{Rel}{W}$
5 brrelex12 ${⊢}\left(\mathrm{Rel}{W}\wedge {X}{W}{R}\right)\to \left({X}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)$
6 4 5 sylan ${⊢}\left({\phi }\wedge {X}{W}{R}\right)\to \left({X}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)$
7 2 adantr ${⊢}\left({\phi }\wedge \left(\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\wedge \left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right)\to {A}\in \mathrm{V}$
8 simprll ${⊢}\left({\phi }\wedge \left(\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\wedge \left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right)\to {X}\subseteq {A}$
9 7 8 ssexd ${⊢}\left({\phi }\wedge \left(\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\wedge \left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right)\to {X}\in \mathrm{V}$
10 9 9 xpexd ${⊢}\left({\phi }\wedge \left(\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\wedge \left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right)\to {X}×{X}\in \mathrm{V}$
11 simprlr ${⊢}\left({\phi }\wedge \left(\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\wedge \left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right)\to {R}\subseteq {X}×{X}$
12 10 11 ssexd ${⊢}\left({\phi }\wedge \left(\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\wedge \left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right)\to {R}\in \mathrm{V}$
13 9 12 jca ${⊢}\left({\phi }\wedge \left(\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\wedge \left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right)\to \left({X}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)$
14 simpl ${⊢}\left({x}={X}\wedge {r}={R}\right)\to {x}={X}$
15 14 sseq1d ${⊢}\left({x}={X}\wedge {r}={R}\right)\to \left({x}\subseteq {A}↔{X}\subseteq {A}\right)$
16 simpr ${⊢}\left({x}={X}\wedge {r}={R}\right)\to {r}={R}$
17 14 sqxpeqd ${⊢}\left({x}={X}\wedge {r}={R}\right)\to {x}×{x}={X}×{X}$
18 16 17 sseq12d ${⊢}\left({x}={X}\wedge {r}={R}\right)\to \left({r}\subseteq {x}×{x}↔{R}\subseteq {X}×{X}\right)$
19 15 18 anbi12d ${⊢}\left({x}={X}\wedge {r}={R}\right)\to \left(\left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\right)↔\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\right)$
20 weeq2 ${⊢}{x}={X}\to \left({r}\mathrm{We}{x}↔{r}\mathrm{We}{X}\right)$
21 weeq1 ${⊢}{r}={R}\to \left({r}\mathrm{We}{X}↔{R}\mathrm{We}{X}\right)$
22 20 21 sylan9bb ${⊢}\left({x}={X}\wedge {r}={R}\right)\to \left({r}\mathrm{We}{x}↔{R}\mathrm{We}{X}\right)$
23 16 cnveqd ${⊢}\left({x}={X}\wedge {r}={R}\right)\to {{r}}^{-1}={{R}}^{-1}$
24 23 imaeq1d ${⊢}\left({x}={X}\wedge {r}={R}\right)\to {{r}}^{-1}\left[\left\{{y}\right\}\right]={{R}}^{-1}\left[\left\{{y}\right\}\right]$
25 24 fveqeq2d ${⊢}\left({x}={X}\wedge {r}={R}\right)\to \left({F}\left({{r}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}↔{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)$
26 14 25 raleqbidv ${⊢}\left({x}={X}\wedge {r}={R}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{F}\left({{r}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)$
27 22 26 anbi12d ${⊢}\left({x}={X}\wedge {r}={R}\right)\to \left(\left({r}\mathrm{We}{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{F}\left({{r}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)↔\left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)$
28 19 27 anbi12d ${⊢}\left({x}={X}\wedge {r}={R}\right)\to \left(\left(\left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\right)\wedge \left({r}\mathrm{We}{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{F}\left({{r}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)↔\left(\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\wedge \left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right)$
29 28 1 brabga ${⊢}\left({X}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to \left({X}{W}{R}↔\left(\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\wedge \left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right)$
30 6 13 29 pm5.21nd ${⊢}{\phi }\to \left({X}{W}{R}↔\left(\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\right)\wedge \left({R}\mathrm{We}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({{R}}^{-1}\left[\left\{{y}\right\}\right]\right)={y}\right)\right)\right)$