# Metamath Proof Explorer

## Theorem fpwwe2lem5

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

Ref Expression
Hypotheses fpwwe2.1
fpwwe2.2 ${⊢}{\phi }\to {A}\in \mathrm{V}$
fpwwe2.3 ${⊢}\left({\phi }\wedge \left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\wedge {r}\mathrm{We}{x}\right)\right)\to {x}{F}{r}\in {A}$
Assertion fpwwe2lem5 ${⊢}\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\to {X}{F}{R}\in {A}$

### Proof

Step Hyp Ref Expression
1 fpwwe2.1
2 fpwwe2.2 ${⊢}{\phi }\to {A}\in \mathrm{V}$
3 fpwwe2.3 ${⊢}\left({\phi }\wedge \left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\wedge {r}\mathrm{We}{x}\right)\right)\to {x}{F}{r}\in {A}$
4 2 adantr ${⊢}\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\to {A}\in \mathrm{V}$
5 simpr1 ${⊢}\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\to {X}\subseteq {A}$
6 4 5 ssexd ${⊢}\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\to {X}\in \mathrm{V}$
7 6 6 xpexd ${⊢}\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\to {X}×{X}\in \mathrm{V}$
8 simpr2 ${⊢}\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\to {R}\subseteq {X}×{X}$
9 7 8 ssexd ${⊢}\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\to {R}\in \mathrm{V}$
10 6 9 jca ${⊢}\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\to \left({X}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)$
11 sseq1 ${⊢}{x}={X}\to \left({x}\subseteq {A}↔{X}\subseteq {A}\right)$
12 xpeq12 ${⊢}\left({x}={X}\wedge {x}={X}\right)\to {x}×{x}={X}×{X}$
13 12 anidms ${⊢}{x}={X}\to {x}×{x}={X}×{X}$
14 13 sseq2d ${⊢}{x}={X}\to \left({r}\subseteq {x}×{x}↔{r}\subseteq {X}×{X}\right)$
15 weeq2 ${⊢}{x}={X}\to \left({r}\mathrm{We}{x}↔{r}\mathrm{We}{X}\right)$
16 11 14 15 3anbi123d ${⊢}{x}={X}\to \left(\left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\wedge {r}\mathrm{We}{x}\right)↔\left({X}\subseteq {A}\wedge {r}\subseteq {X}×{X}\wedge {r}\mathrm{We}{X}\right)\right)$
17 16 anbi2d ${⊢}{x}={X}\to \left(\left({\phi }\wedge \left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\wedge {r}\mathrm{We}{x}\right)\right)↔\left({\phi }\wedge \left({X}\subseteq {A}\wedge {r}\subseteq {X}×{X}\wedge {r}\mathrm{We}{X}\right)\right)\right)$
18 oveq1 ${⊢}{x}={X}\to {x}{F}{r}={X}{F}{r}$
19 18 eleq1d ${⊢}{x}={X}\to \left({x}{F}{r}\in {A}↔{X}{F}{r}\in {A}\right)$
20 17 19 imbi12d ${⊢}{x}={X}\to \left(\left(\left({\phi }\wedge \left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\wedge {r}\mathrm{We}{x}\right)\right)\to {x}{F}{r}\in {A}\right)↔\left(\left({\phi }\wedge \left({X}\subseteq {A}\wedge {r}\subseteq {X}×{X}\wedge {r}\mathrm{We}{X}\right)\right)\to {X}{F}{r}\in {A}\right)\right)$
21 sseq1 ${⊢}{r}={R}\to \left({r}\subseteq {X}×{X}↔{R}\subseteq {X}×{X}\right)$
22 weeq1 ${⊢}{r}={R}\to \left({r}\mathrm{We}{X}↔{R}\mathrm{We}{X}\right)$
23 21 22 3anbi23d ${⊢}{r}={R}\to \left(\left({X}\subseteq {A}\wedge {r}\subseteq {X}×{X}\wedge {r}\mathrm{We}{X}\right)↔\left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)$
24 23 anbi2d ${⊢}{r}={R}\to \left(\left({\phi }\wedge \left({X}\subseteq {A}\wedge {r}\subseteq {X}×{X}\wedge {r}\mathrm{We}{X}\right)\right)↔\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\right)$
25 oveq2 ${⊢}{r}={R}\to {X}{F}{r}={X}{F}{R}$
26 25 eleq1d ${⊢}{r}={R}\to \left({X}{F}{r}\in {A}↔{X}{F}{R}\in {A}\right)$
27 24 26 imbi12d ${⊢}{r}={R}\to \left(\left(\left({\phi }\wedge \left({X}\subseteq {A}\wedge {r}\subseteq {X}×{X}\wedge {r}\mathrm{We}{X}\right)\right)\to {X}{F}{r}\in {A}\right)↔\left(\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\to {X}{F}{R}\in {A}\right)\right)$
28 20 27 3 vtocl2g ${⊢}\left({X}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to \left(\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\to {X}{F}{R}\in {A}\right)$
29 10 28 mpcom ${⊢}\left({\phi }\wedge \left({X}\subseteq {A}\wedge {R}\subseteq {X}×{X}\wedge {R}\mathrm{We}{X}\right)\right)\to {X}{F}{R}\in {A}$