# Metamath Proof Explorer

## Theorem fpwwe2lem12

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 18-May-2015) (Proof shortened by Peter Mazsa, 23-Sep-2022)

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}$
fpwwe2.4 ${⊢}{X}=\bigcup \mathrm{dom}{W}$
Assertion fpwwe2lem12 ${⊢}{\phi }\to {X}\in \mathrm{dom}{W}$

### 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 fpwwe2.4 ${⊢}{X}=\bigcup \mathrm{dom}{W}$
5 vex ${⊢}{a}\in \mathrm{V}$
6 5 eldm ${⊢}{a}\in \mathrm{dom}{W}↔\exists {s}\phantom{\rule{.4em}{0ex}}{a}{W}{s}$
7 1 2 fpwwe2lem2
8 7 simprbda ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to \left({a}\subseteq {A}\wedge {s}\subseteq {a}×{a}\right)$
9 8 simpld ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {a}\subseteq {A}$
10 velpw ${⊢}{a}\in 𝒫{A}↔{a}\subseteq {A}$
11 9 10 sylibr ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {a}\in 𝒫{A}$
12 11 ex ${⊢}{\phi }\to \left({a}{W}{s}\to {a}\in 𝒫{A}\right)$
13 12 exlimdv ${⊢}{\phi }\to \left(\exists {s}\phantom{\rule{.4em}{0ex}}{a}{W}{s}\to {a}\in 𝒫{A}\right)$
14 6 13 syl5bi ${⊢}{\phi }\to \left({a}\in \mathrm{dom}{W}\to {a}\in 𝒫{A}\right)$
15 14 ssrdv ${⊢}{\phi }\to \mathrm{dom}{W}\subseteq 𝒫{A}$
16 sspwuni ${⊢}\mathrm{dom}{W}\subseteq 𝒫{A}↔\bigcup \mathrm{dom}{W}\subseteq {A}$
17 15 16 sylib ${⊢}{\phi }\to \bigcup \mathrm{dom}{W}\subseteq {A}$
18 4 17 eqsstrid ${⊢}{\phi }\to {X}\subseteq {A}$
19 vex ${⊢}{s}\in \mathrm{V}$
20 19 elrn ${⊢}{s}\in \mathrm{ran}{W}↔\exists {a}\phantom{\rule{.4em}{0ex}}{a}{W}{s}$
21 8 simprd ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {s}\subseteq {a}×{a}$
22 1 relopabi ${⊢}\mathrm{Rel}{W}$
23 22 releldmi ${⊢}{a}{W}{s}\to {a}\in \mathrm{dom}{W}$
24 23 adantl ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {a}\in \mathrm{dom}{W}$
25 elssuni ${⊢}{a}\in \mathrm{dom}{W}\to {a}\subseteq \bigcup \mathrm{dom}{W}$
26 24 25 syl ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {a}\subseteq \bigcup \mathrm{dom}{W}$
27 26 4 sseqtrrdi ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {a}\subseteq {X}$
28 xpss12 ${⊢}\left({a}\subseteq {X}\wedge {a}\subseteq {X}\right)\to {a}×{a}\subseteq {X}×{X}$
29 27 27 28 syl2anc ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {a}×{a}\subseteq {X}×{X}$
30 21 29 sstrd ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {s}\subseteq {X}×{X}$
31 velpw ${⊢}{s}\in 𝒫\left({X}×{X}\right)↔{s}\subseteq {X}×{X}$
32 30 31 sylibr ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {s}\in 𝒫\left({X}×{X}\right)$
33 32 ex ${⊢}{\phi }\to \left({a}{W}{s}\to {s}\in 𝒫\left({X}×{X}\right)\right)$
34 33 exlimdv ${⊢}{\phi }\to \left(\exists {a}\phantom{\rule{.4em}{0ex}}{a}{W}{s}\to {s}\in 𝒫\left({X}×{X}\right)\right)$
35 20 34 syl5bi ${⊢}{\phi }\to \left({s}\in \mathrm{ran}{W}\to {s}\in 𝒫\left({X}×{X}\right)\right)$
36 35 ssrdv ${⊢}{\phi }\to \mathrm{ran}{W}\subseteq 𝒫\left({X}×{X}\right)$
37 sspwuni ${⊢}\mathrm{ran}{W}\subseteq 𝒫\left({X}×{X}\right)↔\bigcup \mathrm{ran}{W}\subseteq {X}×{X}$
38 36 37 sylib ${⊢}{\phi }\to \bigcup \mathrm{ran}{W}\subseteq {X}×{X}$
39 18 38 jca ${⊢}{\phi }\to \left({X}\subseteq {A}\wedge \bigcup \mathrm{ran}{W}\subseteq {X}×{X}\right)$
40 n0 ${⊢}{n}\ne \varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {n}$
41 ssel2 ${⊢}\left({n}\subseteq {X}\wedge {y}\in {n}\right)\to {y}\in {X}$
42 41 adantl ${⊢}\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\to {y}\in {X}$
43 4 eleq2i ${⊢}{y}\in {X}↔{y}\in \bigcup \mathrm{dom}{W}$
44 eluni2 ${⊢}{y}\in \bigcup \mathrm{dom}{W}↔\exists {a}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}{y}\in {a}$
45 43 44 bitri ${⊢}{y}\in {X}↔\exists {a}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}{y}\in {a}$
46 42 45 sylib ${⊢}\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\to \exists {a}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}{y}\in {a}$
47 5 inex2 ${⊢}{n}\cap {a}\in \mathrm{V}$
48 47 a1i ${⊢}\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {n}\cap {a}\in \mathrm{V}$
49 7 simplbda
50 49 simpld ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {s}\mathrm{We}{a}$
51 50 ad2ant2r ${⊢}\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {s}\mathrm{We}{a}$
52 wefr ${⊢}{s}\mathrm{We}{a}\to {s}\mathrm{Fr}{a}$
53 51 52 syl ${⊢}\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {s}\mathrm{Fr}{a}$
54 inss2 ${⊢}{n}\cap {a}\subseteq {a}$
55 54 a1i ${⊢}\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {n}\cap {a}\subseteq {a}$
56 simplrr ${⊢}\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {y}\in {n}$
57 simprr ${⊢}\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {y}\in {a}$
58 inelcm ${⊢}\left({y}\in {n}\wedge {y}\in {a}\right)\to {n}\cap {a}\ne \varnothing$
59 56 57 58 syl2anc ${⊢}\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {n}\cap {a}\ne \varnothing$
60 fri ${⊢}\left(\left({n}\cap {a}\in \mathrm{V}\wedge {s}\mathrm{Fr}{a}\right)\wedge \left({n}\cap {a}\subseteq {a}\wedge {n}\cap {a}\ne \varnothing \right)\right)\to \exists {v}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}$
61 48 53 55 59 60 syl22anc ${⊢}\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \exists {v}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}$
62 simprl ${⊢}\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\to {v}\in \left({n}\cap {a}\right)$
63 62 elin1d ${⊢}\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\to {v}\in {n}$
64 simplrr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge {w}\in {n}\right)\to \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}$
65 ralnex ${⊢}\forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}↔¬\exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}$
66 64 65 sylib ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge {w}\in {n}\right)\to ¬\exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}$
67 df-br ${⊢}{w}\bigcup \mathrm{ran}{W}{v}↔⟨{w},{v}⟩\in \bigcup \mathrm{ran}{W}$
68 eluni2 ${⊢}⟨{w},{v}⟩\in \bigcup \mathrm{ran}{W}↔\exists {t}\in \mathrm{ran}{W}\phantom{\rule{.4em}{0ex}}⟨{w},{v}⟩\in {t}$
69 67 68 bitri ${⊢}{w}\bigcup \mathrm{ran}{W}{v}↔\exists {t}\in \mathrm{ran}{W}\phantom{\rule{.4em}{0ex}}⟨{w},{v}⟩\in {t}$
70 vex ${⊢}{t}\in \mathrm{V}$
71 70 elrn ${⊢}{t}\in \mathrm{ran}{W}↔\exists {b}\phantom{\rule{.4em}{0ex}}{b}{W}{t}$
72 df-br ${⊢}{w}{t}{v}↔⟨{w},{v}⟩\in {t}$
73 simprll ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to {w}\in {n}$
74 73 adantr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {w}\in {n}$
75 simprr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to {w}{t}{v}$
76 simp-4l ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to {\phi }$
77 simprl ${⊢}\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {a}{W}{s}$
78 77 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to {a}{W}{s}$
79 simprlr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to {b}{W}{t}$
80 simprr ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to {b}{W}{t}$
81 1 2 fpwwe2lem2
83 80 82 mpbid
84 83 simpld ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to \left({b}\subseteq {A}\wedge {t}\subseteq {b}×{b}\right)$
85 84 simprd ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to {t}\subseteq {b}×{b}$
86 76 78 79 85 syl12anc ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to {t}\subseteq {b}×{b}$
87 86 ssbrd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to \left({w}{t}{v}\to {w}\left({b}×{b}\right){v}\right)$
88 75 87 mpd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to {w}\left({b}×{b}\right){v}$
89 brxp ${⊢}{w}\left({b}×{b}\right){v}↔\left({w}\in {b}\wedge {v}\in {b}\right)$
90 89 simplbi ${⊢}{w}\left({b}×{b}\right){v}\to {w}\in {b}$
91 88 90 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to {w}\in {b}$
92 91 adantr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {w}\in {b}$
93 62 elin2d ${⊢}\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\to {v}\in {a}$
94 93 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {v}\in {a}$
95 simplrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {w}{t}{v}$
96 brinxp2 ${⊢}{w}\left({t}\cap \left({b}×{a}\right)\right){v}↔\left(\left({w}\in {b}\wedge {v}\in {a}\right)\wedge {w}{t}{v}\right)$
97 92 94 95 96 syl21anbrc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {w}\left({t}\cap \left({b}×{a}\right)\right){v}$
98 simprr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {s}={t}\cap \left({b}×{a}\right)$
99 98 breqd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({w}{s}{v}↔{w}\left({t}\cap \left({b}×{a}\right)\right){v}\right)$
100 97 99 mpbird ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {w}{s}{v}$
101 76 78 21 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to {s}\subseteq {a}×{a}$
102 101 adantr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {s}\subseteq {a}×{a}$
103 102 ssbrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({w}{s}{v}\to {w}\left({a}×{a}\right){v}\right)$
104 100 103 mpd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {w}\left({a}×{a}\right){v}$
105 brxp ${⊢}{w}\left({a}×{a}\right){v}↔\left({w}\in {a}\wedge {v}\in {a}\right)$
106 105 simplbi ${⊢}{w}\left({a}×{a}\right){v}\to {w}\in {a}$
107 104 106 syl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {w}\in {a}$
108 74 107 elind ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {w}\in \left({n}\cap {a}\right)$
109 breq1 ${⊢}{z}={w}\to \left({z}{s}{v}↔{w}{s}{v}\right)$
110 109 rspcev ${⊢}\left({w}\in \left({n}\cap {a}\right)\wedge {w}{s}{v}\right)\to \exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}$
111 108 100 110 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}$
112 73 adantr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {w}\in {n}$
113 simprl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {b}\subseteq {a}$
114 91 adantr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {w}\in {b}$
115 113 114 sseldd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {w}\in {a}$
116 112 115 elind ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {w}\in \left({n}\cap {a}\right)$
117 simplrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {w}{t}{v}$
118 simprr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {t}={s}\cap \left({a}×{b}\right)$
119 inss1 ${⊢}{s}\cap \left({a}×{b}\right)\subseteq {s}$
120 118 119 eqsstrdi ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {t}\subseteq {s}$
121 120 ssbrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to \left({w}{t}{v}\to {w}{s}{v}\right)$
122 117 121 mpd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {w}{s}{v}$
123 116 122 110 syl2anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to \exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}$
124 2 adantr ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to {A}\in \mathrm{V}$
125 3 adantlr ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({x}\subseteq {A}\wedge {r}\subseteq {x}×{x}\wedge {r}\mathrm{We}{x}\right)\right)\to {x}{F}{r}\in {A}$
126 simprl ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to {a}{W}{s}$
127 1 124 125 126 80 fpwwe2lem10 ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to \left(\left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\vee \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)$
128 76 78 79 127 syl12anc ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to \left(\left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\vee \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)$
129 111 123 128 mpjaodan ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left(\left({w}\in {n}\wedge {b}{W}{t}\right)\wedge {w}{t}{v}\right)\right)\to \exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}$
130 129 expr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left({w}\in {n}\wedge {b}{W}{t}\right)\right)\to \left({w}{t}{v}\to \exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}\right)$
131 72 130 syl5bir ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge \left({w}\in {n}\wedge {b}{W}{t}\right)\right)\to \left(⟨{w},{v}⟩\in {t}\to \exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}\right)$
132 131 expr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge {w}\in {n}\right)\to \left({b}{W}{t}\to \left(⟨{w},{v}⟩\in {t}\to \exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}\right)\right)$
133 132 exlimdv ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge {w}\in {n}\right)\to \left(\exists {b}\phantom{\rule{.4em}{0ex}}{b}{W}{t}\to \left(⟨{w},{v}⟩\in {t}\to \exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}\right)\right)$
134 71 133 syl5bi ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge {w}\in {n}\right)\to \left({t}\in \mathrm{ran}{W}\to \left(⟨{w},{v}⟩\in {t}\to \exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}\right)\right)$
135 134 rexlimdv ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge {w}\in {n}\right)\to \left(\exists {t}\in \mathrm{ran}{W}\phantom{\rule{.4em}{0ex}}⟨{w},{v}⟩\in {t}\to \exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}\right)$
136 69 135 syl5bi ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge {w}\in {n}\right)\to \left({w}\bigcup \mathrm{ran}{W}{v}\to \exists {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}{z}{s}{v}\right)$
137 66 136 mtod ${⊢}\left(\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\wedge {w}\in {n}\right)\to ¬{w}\bigcup \mathrm{ran}{W}{v}$
138 137 ralrimiva ${⊢}\left(\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({v}\in \left({n}\cap {a}\right)\wedge \forall {z}\in \left({n}\cap {a}\right)\phantom{\rule{.4em}{0ex}}¬{z}{s}{v}\right)\right)\to \forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}$
139 61 63 138 reximssdv ${⊢}\left(\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}$
140 139 exp32 ${⊢}\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\to \left({a}{W}{s}\to \left({y}\in {a}\to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}\right)\right)$
141 140 exlimdv ${⊢}\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\to \left(\exists {s}\phantom{\rule{.4em}{0ex}}{a}{W}{s}\to \left({y}\in {a}\to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}\right)\right)$
142 6 141 syl5bi ${⊢}\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\to \left({a}\in \mathrm{dom}{W}\to \left({y}\in {a}\to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}\right)\right)$
143 142 rexlimdv ${⊢}\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\to \left(\exists {a}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}{y}\in {a}\to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}\right)$
144 46 143 mpd ${⊢}\left({\phi }\wedge \left({n}\subseteq {X}\wedge {y}\in {n}\right)\right)\to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}$
145 144 expr ${⊢}\left({\phi }\wedge {n}\subseteq {X}\right)\to \left({y}\in {n}\to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}\right)$
146 145 exlimdv ${⊢}\left({\phi }\wedge {n}\subseteq {X}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {n}\to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}\right)$
147 40 146 syl5bi ${⊢}\left({\phi }\wedge {n}\subseteq {X}\right)\to \left({n}\ne \varnothing \to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}\right)$
148 147 expimpd ${⊢}{\phi }\to \left(\left({n}\subseteq {X}\wedge {n}\ne \varnothing \right)\to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}\right)$
149 148 alrimiv ${⊢}{\phi }\to \forall {n}\phantom{\rule{.4em}{0ex}}\left(\left({n}\subseteq {X}\wedge {n}\ne \varnothing \right)\to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}\right)$
150 df-fr ${⊢}\bigcup \mathrm{ran}{W}\mathrm{Fr}{X}↔\forall {n}\phantom{\rule{.4em}{0ex}}\left(\left({n}\subseteq {X}\wedge {n}\ne \varnothing \right)\to \exists {v}\in {n}\phantom{\rule{.4em}{0ex}}\forall {w}\in {n}\phantom{\rule{.4em}{0ex}}¬{w}\bigcup \mathrm{ran}{W}{v}\right)$
151 149 150 sylibr ${⊢}{\phi }\to \bigcup \mathrm{ran}{W}\mathrm{Fr}{X}$
152 4 eleq2i ${⊢}{w}\in {X}↔{w}\in \bigcup \mathrm{dom}{W}$
153 eluni2 ${⊢}{w}\in \bigcup \mathrm{dom}{W}↔\exists {b}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}{w}\in {b}$
154 152 153 bitri ${⊢}{w}\in {X}↔\exists {b}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}{w}\in {b}$
155 45 154 anbi12i ${⊢}\left({y}\in {X}\wedge {w}\in {X}\right)↔\left(\exists {a}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}{y}\in {a}\wedge \exists {b}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}{w}\in {b}\right)$
156 reeanv ${⊢}\exists {a}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}\left({y}\in {a}\wedge {w}\in {b}\right)↔\left(\exists {a}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}{y}\in {a}\wedge \exists {b}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}{w}\in {b}\right)$
157 155 156 bitr4i ${⊢}\left({y}\in {X}\wedge {w}\in {X}\right)↔\exists {a}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}\left({y}\in {a}\wedge {w}\in {b}\right)$
158 vex ${⊢}{b}\in \mathrm{V}$
159 158 eldm ${⊢}{b}\in \mathrm{dom}{W}↔\exists {t}\phantom{\rule{.4em}{0ex}}{b}{W}{t}$
160 6 159 anbi12i ${⊢}\left({a}\in \mathrm{dom}{W}\wedge {b}\in \mathrm{dom}{W}\right)↔\left(\exists {s}\phantom{\rule{.4em}{0ex}}{a}{W}{s}\wedge \exists {t}\phantom{\rule{.4em}{0ex}}{b}{W}{t}\right)$
161 exdistrv ${⊢}\exists {s}\phantom{\rule{.4em}{0ex}}\exists {t}\phantom{\rule{.4em}{0ex}}\left({a}{W}{s}\wedge {b}{W}{t}\right)↔\left(\exists {s}\phantom{\rule{.4em}{0ex}}{a}{W}{s}\wedge \exists {t}\phantom{\rule{.4em}{0ex}}{b}{W}{t}\right)$
162 160 161 bitr4i ${⊢}\left({a}\in \mathrm{dom}{W}\wedge {b}\in \mathrm{dom}{W}\right)↔\exists {s}\phantom{\rule{.4em}{0ex}}\exists {t}\phantom{\rule{.4em}{0ex}}\left({a}{W}{s}\wedge {b}{W}{t}\right)$
163 83 simprd
164 163 simpld ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to {t}\mathrm{We}{b}$
165 164 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {t}\mathrm{We}{b}$
166 weso ${⊢}{t}\mathrm{We}{b}\to {t}\mathrm{Or}{b}$
167 165 166 syl ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {t}\mathrm{Or}{b}$
168 simprl ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {a}\subseteq {b}$
169 simplrl ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {y}\in {a}$
170 168 169 sseldd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {y}\in {b}$
171 simplrr ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {w}\in {b}$
172 solin ${⊢}\left({t}\mathrm{Or}{b}\wedge \left({y}\in {b}\wedge {w}\in {b}\right)\right)\to \left({y}{t}{w}\vee {y}={w}\vee {w}{t}{y}\right)$
173 167 170 171 172 syl12anc ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({y}{t}{w}\vee {y}={w}\vee {w}{t}{y}\right)$
174 22 relelrni ${⊢}{b}{W}{t}\to {t}\in \mathrm{ran}{W}$
175 174 ad2antll ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to {t}\in \mathrm{ran}{W}$
176 175 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {t}\in \mathrm{ran}{W}$
177 elssuni ${⊢}{t}\in \mathrm{ran}{W}\to {t}\subseteq \bigcup \mathrm{ran}{W}$
178 176 177 syl ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {t}\subseteq \bigcup \mathrm{ran}{W}$
179 178 ssbrd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({y}{t}{w}\to {y}\bigcup \mathrm{ran}{W}{w}\right)$
180 idd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({y}={w}\to {y}={w}\right)$
181 178 ssbrd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({w}{t}{y}\to {w}\bigcup \mathrm{ran}{W}{y}\right)$
182 179 180 181 3orim123d ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left(\left({y}{t}{w}\vee {y}={w}\vee {w}{t}{y}\right)\to \left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)\right)$
183 173 182 mpd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)$
184 50 adantrr ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to {s}\mathrm{We}{a}$
185 184 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {s}\mathrm{We}{a}$
186 weso ${⊢}{s}\mathrm{We}{a}\to {s}\mathrm{Or}{a}$
187 185 186 syl ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {s}\mathrm{Or}{a}$
188 simplrl ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {y}\in {a}$
189 simprl ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {b}\subseteq {a}$
190 simplrr ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {w}\in {b}$
191 189 190 sseldd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {w}\in {a}$
192 solin ${⊢}\left({s}\mathrm{Or}{a}\wedge \left({y}\in {a}\wedge {w}\in {a}\right)\right)\to \left({y}{s}{w}\vee {y}={w}\vee {w}{s}{y}\right)$
193 187 188 191 192 syl12anc ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to \left({y}{s}{w}\vee {y}={w}\vee {w}{s}{y}\right)$
194 22 relelrni ${⊢}{a}{W}{s}\to {s}\in \mathrm{ran}{W}$
195 194 ad2antrl ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to {s}\in \mathrm{ran}{W}$
196 195 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {s}\in \mathrm{ran}{W}$
197 elssuni ${⊢}{s}\in \mathrm{ran}{W}\to {s}\subseteq \bigcup \mathrm{ran}{W}$
198 196 197 syl ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {s}\subseteq \bigcup \mathrm{ran}{W}$
199 198 ssbrd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to \left({y}{s}{w}\to {y}\bigcup \mathrm{ran}{W}{w}\right)$
200 idd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to \left({y}={w}\to {y}={w}\right)$
201 198 ssbrd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to \left({w}{s}{y}\to {w}\bigcup \mathrm{ran}{W}{y}\right)$
202 199 200 201 3orim123d ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to \left(\left({y}{s}{w}\vee {y}={w}\vee {w}{s}{y}\right)\to \left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)\right)$
203 193 202 mpd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to \left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)$
204 127 adantr ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\to \left(\left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\vee \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)$
205 183 203 204 mpjaodan ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({y}\in {a}\wedge {w}\in {b}\right)\right)\to \left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)$
206 205 exp31 ${⊢}{\phi }\to \left(\left({a}{W}{s}\wedge {b}{W}{t}\right)\to \left(\left({y}\in {a}\wedge {w}\in {b}\right)\to \left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)\right)\right)$
207 206 exlimdvv ${⊢}{\phi }\to \left(\exists {s}\phantom{\rule{.4em}{0ex}}\exists {t}\phantom{\rule{.4em}{0ex}}\left({a}{W}{s}\wedge {b}{W}{t}\right)\to \left(\left({y}\in {a}\wedge {w}\in {b}\right)\to \left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)\right)\right)$
208 162 207 syl5bi ${⊢}{\phi }\to \left(\left({a}\in \mathrm{dom}{W}\wedge {b}\in \mathrm{dom}{W}\right)\to \left(\left({y}\in {a}\wedge {w}\in {b}\right)\to \left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)\right)\right)$
209 208 rexlimdvv ${⊢}{\phi }\to \left(\exists {a}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{dom}{W}\phantom{\rule{.4em}{0ex}}\left({y}\in {a}\wedge {w}\in {b}\right)\to \left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)\right)$
210 157 209 syl5bi ${⊢}{\phi }\to \left(\left({y}\in {X}\wedge {w}\in {X}\right)\to \left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)\right)$
211 210 ralrimivv ${⊢}{\phi }\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {w}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)$
212 dfwe2 ${⊢}\bigcup \mathrm{ran}{W}\mathrm{We}{X}↔\left(\bigcup \mathrm{ran}{W}\mathrm{Fr}{X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {w}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}\bigcup \mathrm{ran}{W}{w}\vee {y}={w}\vee {w}\bigcup \mathrm{ran}{W}{y}\right)\right)$
213 151 211 212 sylanbrc ${⊢}{\phi }\to \bigcup \mathrm{ran}{W}\mathrm{We}{X}$
214 1 fpwwe2cbv
215 2 adantr ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {A}\in \mathrm{V}$
216 simpr ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to {a}{W}{s}$
217 214 215 216 fpwwe2lem3 ${⊢}\left(\left({\phi }\wedge {a}{W}{s}\right)\wedge {y}\in {a}\right)\to {{s}}^{-1}\left[\left\{{y}\right\}\right]{F}\left({s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)={y}$
218 217 anasss ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {{s}}^{-1}\left[\left\{{y}\right\}\right]{F}\left({s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)={y}$
219 cnvimass ${⊢}{\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\subseteq \mathrm{dom}\bigcup \mathrm{ran}{W}$
220 2 18 ssexd ${⊢}{\phi }\to {X}\in \mathrm{V}$
221 220 220 xpexd ${⊢}{\phi }\to {X}×{X}\in \mathrm{V}$
222 221 38 ssexd ${⊢}{\phi }\to \bigcup \mathrm{ran}{W}\in \mathrm{V}$
223 222 adantr ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \bigcup \mathrm{ran}{W}\in \mathrm{V}$
224 223 dmexd ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \mathrm{dom}\bigcup \mathrm{ran}{W}\in \mathrm{V}$
225 ssexg ${⊢}\left({\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\subseteq \mathrm{dom}\bigcup \mathrm{ran}{W}\wedge \mathrm{dom}\bigcup \mathrm{ran}{W}\in \mathrm{V}\right)\to {\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\in \mathrm{V}$
226 219 224 225 sylancr ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\in \mathrm{V}$
227 id ${⊢}{u}={\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\to {u}={\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]$
228 olc ${⊢}{w}={y}\to \left({w}{s}{y}\vee {w}={y}\right)$
229 df-br ${⊢}{z}\bigcup \mathrm{ran}{W}{w}↔⟨{z},{w}⟩\in \bigcup \mathrm{ran}{W}$
230 eluni2 ${⊢}⟨{z},{w}⟩\in \bigcup \mathrm{ran}{W}↔\exists {t}\in \mathrm{ran}{W}\phantom{\rule{.4em}{0ex}}⟨{z},{w}⟩\in {t}$
231 229 230 bitri ${⊢}{z}\bigcup \mathrm{ran}{W}{w}↔\exists {t}\in \mathrm{ran}{W}\phantom{\rule{.4em}{0ex}}⟨{z},{w}⟩\in {t}$
232 df-br ${⊢}{z}{t}{w}↔⟨{z},{w}⟩\in {t}$
233 85 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {t}\subseteq {b}×{b}$
234 233 ssbrd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({z}{t}{w}\to {z}\left({b}×{b}\right){w}\right)$
235 brxp ${⊢}{z}\left({b}×{b}\right){w}↔\left({z}\in {b}\wedge {w}\in {b}\right)$
236 235 simplbi ${⊢}{z}\left({b}×{b}\right){w}\to {z}\in {b}$
237 234 236 syl6 ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({z}{t}{w}\to {z}\in {b}\right)$
238 21 adantrr ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to {s}\subseteq {a}×{a}$
239 238 ssbrd ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to \left({w}{s}{y}\to {w}\left({a}×{a}\right){y}\right)$
240 239 imp ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge {w}{s}{y}\right)\to {w}\left({a}×{a}\right){y}$
241 brxp ${⊢}{w}\left({a}×{a}\right){y}↔\left({w}\in {a}\wedge {y}\in {a}\right)$
242 241 simplbi ${⊢}{w}\left({a}×{a}\right){y}\to {w}\in {a}$
243 240 242 syl ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge {w}{s}{y}\right)\to {w}\in {a}$
244 243 a1d ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge {w}{s}{y}\right)\to \left({y}\in {a}\to {w}\in {a}\right)$
245 elequ1 ${⊢}{w}={y}\to \left({w}\in {a}↔{y}\in {a}\right)$
246 245 biimprd ${⊢}{w}={y}\to \left({y}\in {a}\to {w}\in {a}\right)$
247 246 adantl ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge {w}={y}\right)\to \left({y}\in {a}\to {w}\in {a}\right)$
248 244 247 jaodan ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left({w}{s}{y}\vee {w}={y}\right)\right)\to \left({y}\in {a}\to {w}\in {a}\right)$
249 248 impr ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\to {w}\in {a}$
250 249 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {w}\in {a}$
251 237 250 jctird ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({z}{t}{w}\to \left({z}\in {b}\wedge {w}\in {a}\right)\right)$
252 brxp ${⊢}{z}\left({b}×{a}\right){w}↔\left({z}\in {b}\wedge {w}\in {a}\right)$
253 251 252 syl6ibr ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({z}{t}{w}\to {z}\left({b}×{a}\right){w}\right)$
254 253 ancld ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({z}{t}{w}\to \left({z}{t}{w}\wedge {z}\left({b}×{a}\right){w}\right)\right)$
255 simprr ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to {s}={t}\cap \left({b}×{a}\right)$
256 255 breqd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({z}{s}{w}↔{z}\left({t}\cap \left({b}×{a}\right)\right){w}\right)$
257 brin ${⊢}{z}\left({t}\cap \left({b}×{a}\right)\right){w}↔\left({z}{t}{w}\wedge {z}\left({b}×{a}\right){w}\right)$
258 256 257 syl6bb ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({z}{s}{w}↔\left({z}{t}{w}\wedge {z}\left({b}×{a}\right){w}\right)\right)$
259 254 258 sylibrd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\right)\to \left({z}{t}{w}\to {z}{s}{w}\right)$
260 simprr ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {t}={s}\cap \left({a}×{b}\right)$
261 260 119 eqsstrdi ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to {t}\subseteq {s}$
262 261 ssbrd ${⊢}\left(\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\wedge \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)\to \left({z}{t}{w}\to {z}{s}{w}\right)$
263 127 adantr ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\to \left(\left({a}\subseteq {b}\wedge {s}={t}\cap \left({b}×{a}\right)\right)\vee \left({b}\subseteq {a}\wedge {t}={s}\cap \left({a}×{b}\right)\right)\right)$
264 259 262 263 mpjaodan ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\to \left({z}{t}{w}\to {z}{s}{w}\right)$
265 232 264 syl5bir ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\wedge \left(\left({w}{s}{y}\vee {w}={y}\right)\wedge {y}\in {a}\right)\right)\to \left(⟨{z},{w}⟩\in {t}\to {z}{s}{w}\right)$
266 265 exp32 ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {b}{W}{t}\right)\right)\to \left(\left({w}{s}{y}\vee {w}={y}\right)\to \left({y}\in {a}\to \left(⟨{z},{w}⟩\in {t}\to {z}{s}{w}\right)\right)\right)$
267 266 expr ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to \left({b}{W}{t}\to \left(\left({w}{s}{y}\vee {w}={y}\right)\to \left({y}\in {a}\to \left(⟨{z},{w}⟩\in {t}\to {z}{s}{w}\right)\right)\right)\right)$
268 267 com24 ${⊢}\left({\phi }\wedge {a}{W}{s}\right)\to \left({y}\in {a}\to \left(\left({w}{s}{y}\vee {w}={y}\right)\to \left({b}{W}{t}\to \left(⟨{z},{w}⟩\in {t}\to {z}{s}{w}\right)\right)\right)\right)$
269 268 impr ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \left(\left({w}{s}{y}\vee {w}={y}\right)\to \left({b}{W}{t}\to \left(⟨{z},{w}⟩\in {t}\to {z}{s}{w}\right)\right)\right)$
270 269 imp ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({w}{s}{y}\vee {w}={y}\right)\right)\to \left({b}{W}{t}\to \left(⟨{z},{w}⟩\in {t}\to {z}{s}{w}\right)\right)$
271 270 exlimdv ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({w}{s}{y}\vee {w}={y}\right)\right)\to \left(\exists {b}\phantom{\rule{.4em}{0ex}}{b}{W}{t}\to \left(⟨{z},{w}⟩\in {t}\to {z}{s}{w}\right)\right)$
272 71 271 syl5bi ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({w}{s}{y}\vee {w}={y}\right)\right)\to \left({t}\in \mathrm{ran}{W}\to \left(⟨{z},{w}⟩\in {t}\to {z}{s}{w}\right)\right)$
273 272 rexlimdv ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({w}{s}{y}\vee {w}={y}\right)\right)\to \left(\exists {t}\in \mathrm{ran}{W}\phantom{\rule{.4em}{0ex}}⟨{z},{w}⟩\in {t}\to {z}{s}{w}\right)$
274 231 273 syl5bi ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({w}{s}{y}\vee {w}={y}\right)\right)\to \left({z}\bigcup \mathrm{ran}{W}{w}\to {z}{s}{w}\right)$
275 228 274 sylan2 ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge {w}={y}\right)\to \left({z}\bigcup \mathrm{ran}{W}{w}\to {z}{s}{w}\right)$
276 275 ex ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \left({w}={y}\to \left({z}\bigcup \mathrm{ran}{W}{w}\to {z}{s}{w}\right)\right)$
277 276 alrimiv ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \forall {w}\phantom{\rule{.4em}{0ex}}\left({w}={y}\to \left({z}\bigcup \mathrm{ran}{W}{w}\to {z}{s}{w}\right)\right)$
278 breq2 ${⊢}{w}={y}\to \left({z}\bigcup \mathrm{ran}{W}{w}↔{z}\bigcup \mathrm{ran}{W}{y}\right)$
279 breq2 ${⊢}{w}={y}\to \left({z}{s}{w}↔{z}{s}{y}\right)$
280 278 279 imbi12d ${⊢}{w}={y}\to \left(\left({z}\bigcup \mathrm{ran}{W}{w}\to {z}{s}{w}\right)↔\left({z}\bigcup \mathrm{ran}{W}{y}\to {z}{s}{y}\right)\right)$
281 280 equsalvw ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}={y}\to \left({z}\bigcup \mathrm{ran}{W}{w}\to {z}{s}{w}\right)\right)↔\left({z}\bigcup \mathrm{ran}{W}{y}\to {z}{s}{y}\right)$
282 277 281 sylib ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \left({z}\bigcup \mathrm{ran}{W}{y}\to {z}{s}{y}\right)$
283 194 ad2antrl ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {s}\in \mathrm{ran}{W}$
284 283 197 syl ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {s}\subseteq \bigcup \mathrm{ran}{W}$
285 284 ssbrd ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \left({z}{s}{y}\to {z}\bigcup \mathrm{ran}{W}{y}\right)$
286 282 285 impbid ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \left({z}\bigcup \mathrm{ran}{W}{y}↔{z}{s}{y}\right)$
287 vex ${⊢}{z}\in \mathrm{V}$
288 287 eliniseg ${⊢}{y}\in \mathrm{V}\to \left({z}\in {\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]↔{z}\bigcup \mathrm{ran}{W}{y}\right)$
289 288 elv ${⊢}{z}\in {\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]↔{z}\bigcup \mathrm{ran}{W}{y}$
290 287 eliniseg ${⊢}{y}\in \mathrm{V}\to \left({z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]↔{z}{s}{y}\right)$
291 290 elv ${⊢}{z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]↔{z}{s}{y}$
292 286 289 291 3bitr4g ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \left({z}\in {\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]↔{z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\right)$
293 292 eqrdv ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to {\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]={{s}}^{-1}\left[\left\{{y}\right\}\right]$
294 227 293 sylan9eqr ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge {u}={\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\right)\to {u}={{s}}^{-1}\left[\left\{{y}\right\}\right]$
295 294 sqxpeqd ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge {u}={\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\right)\to {u}×{u}={{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]$
296 295 ineq2d ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge {u}={\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\right)\to \bigcup \mathrm{ran}{W}\cap \left({u}×{u}\right)=\bigcup \mathrm{ran}{W}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)$
297 relinxp ${⊢}\mathrm{Rel}\left(\bigcup \mathrm{ran}{W}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)$
298 relinxp ${⊢}\mathrm{Rel}\left({s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)$
299 vex ${⊢}{w}\in \mathrm{V}$
300 299 eliniseg ${⊢}{y}\in \mathrm{V}\to \left({w}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]↔{w}{s}{y}\right)$
301 290 300 anbi12d ${⊢}{y}\in \mathrm{V}\to \left(\left({z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\wedge {w}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\right)↔\left({z}{s}{y}\wedge {w}{s}{y}\right)\right)$
302 301 elv ${⊢}\left({z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\wedge {w}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\right)↔\left({z}{s}{y}\wedge {w}{s}{y}\right)$
303 orc ${⊢}{w}{s}{y}\to \left({w}{s}{y}\vee {w}={y}\right)$
304 303 274 sylan2 ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge {w}{s}{y}\right)\to \left({z}\bigcup \mathrm{ran}{W}{w}\to {z}{s}{w}\right)$
305 304 adantrl ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({z}{s}{y}\wedge {w}{s}{y}\right)\right)\to \left({z}\bigcup \mathrm{ran}{W}{w}\to {z}{s}{w}\right)$
306 284 adantr ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({z}{s}{y}\wedge {w}{s}{y}\right)\right)\to {s}\subseteq \bigcup \mathrm{ran}{W}$
307 306 ssbrd ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({z}{s}{y}\wedge {w}{s}{y}\right)\right)\to \left({z}{s}{w}\to {z}\bigcup \mathrm{ran}{W}{w}\right)$
308 305 307 impbid ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({z}{s}{y}\wedge {w}{s}{y}\right)\right)\to \left({z}\bigcup \mathrm{ran}{W}{w}↔{z}{s}{w}\right)$
309 302 308 sylan2b ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge \left({z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\wedge {w}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)\to \left({z}\bigcup \mathrm{ran}{W}{w}↔{z}{s}{w}\right)$
310 309 pm5.32da ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \left(\left(\left({z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\wedge {w}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\wedge {z}\bigcup \mathrm{ran}{W}{w}\right)↔\left(\left({z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\wedge {w}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\wedge {z}{s}{w}\right)\right)$
311 df-br ${⊢}{z}\left(\bigcup \mathrm{ran}{W}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right){w}↔⟨{z},{w}⟩\in \left(\bigcup \mathrm{ran}{W}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)$
312 brinxp2 ${⊢}{z}\left(\bigcup \mathrm{ran}{W}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right){w}↔\left(\left({z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\wedge {w}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\wedge {z}\bigcup \mathrm{ran}{W}{w}\right)$
313 311 312 bitr3i ${⊢}⟨{z},{w}⟩\in \left(\bigcup \mathrm{ran}{W}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)↔\left(\left({z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\wedge {w}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\wedge {z}\bigcup \mathrm{ran}{W}{w}\right)$
314 df-br ${⊢}{z}\left({s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right){w}↔⟨{z},{w}⟩\in \left({s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)$
315 brinxp2 ${⊢}{z}\left({s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right){w}↔\left(\left({z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\wedge {w}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\wedge {z}{s}{w}\right)$
316 314 315 bitr3i ${⊢}⟨{z},{w}⟩\in \left({s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)↔\left(\left({z}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\wedge {w}\in {{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\wedge {z}{s}{w}\right)$
317 310 313 316 3bitr4g ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \left(⟨{z},{w}⟩\in \left(\bigcup \mathrm{ran}{W}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)↔⟨{z},{w}⟩\in \left({s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)\right)$
318 297 298 317 eqrelrdv ${⊢}\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\to \bigcup \mathrm{ran}{W}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)={s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)$
319 318 adantr ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge {u}={\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\right)\to \bigcup \mathrm{ran}{W}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)={s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)$
320 296 319 eqtrd ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge {u}={\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\right)\to \bigcup \mathrm{ran}{W}\cap \left({u}×{u}\right)={s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)$
321 294 320 oveq12d ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge {u}={\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\right)\to {u}{F}\left(\bigcup \mathrm{ran}{W}\cap \left({u}×{u}\right)\right)={{s}}^{-1}\left[\left\{{y}\right\}\right]{F}\left({s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)$
322 321 eqeq1d ${⊢}\left(\left({\phi }\wedge \left({a}{W}{s}\wedge {y}\in {a}\right)\right)\wedge {u}={\bigcup \mathrm{ran}{W}}^{-1}\left[\left\{{y}\right\}\right]\right)\to \left({u}{F}\left(\bigcup \mathrm{ran}{W}\cap \left({u}×{u}\right)\right)={y}↔{{s}}^{-1}\left[\left\{{y}\right\}\right]{F}\left({s}\cap \left({{s}}^{-1}\left[\left\{{y}\right\}\right]×{{s}}^{-1}\left[\left\{{y}\right\}\right]\right)\right)={y}\right)$
323 226 322 sbcied
324 218 323 mpbird
325 324 exp32
326 325 exlimdv
327 6 326 syl5bi
328 327 rexlimdv
329 45 328 syl5bi
330 329 ralrimiv
331 213 330 jca
332 1 2 fpwwe2lem2
333 39 331 332 mpbir2and ${⊢}{\phi }\to {X}{W}\bigcup \mathrm{ran}{W}$
334 22 releldmi ${⊢}{X}{W}\bigcup \mathrm{ran}{W}\to {X}\in \mathrm{dom}{W}$
335 333 334 syl ${⊢}{\phi }\to {X}\in \mathrm{dom}{W}$