# Metamath Proof Explorer

## Theorem dffv2

Description: Alternate definition of function value df-fv that doesn't require dummy variables. (Contributed by NM, 4-Aug-2010)

Ref Expression
Assertion dffv2 ${⊢}{F}\left({A}\right)=\bigcup \left({F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$

### Proof

Step Hyp Ref Expression
1 snidb ${⊢}{A}\in \mathrm{V}↔{A}\in \left\{{A}\right\}$
2 fvres ${⊢}{A}\in \left\{{A}\right\}\to \left({{F}↾}_{\left\{{A}\right\}}\right)\left({A}\right)={F}\left({A}\right)$
3 1 2 sylbi ${⊢}{A}\in \mathrm{V}\to \left({{F}↾}_{\left\{{A}\right\}}\right)\left({A}\right)={F}\left({A}\right)$
4 fvprc ${⊢}¬{A}\in \mathrm{V}\to \left({{F}↾}_{\left\{{A}\right\}}\right)\left({A}\right)=\varnothing$
5 fvprc ${⊢}¬{A}\in \mathrm{V}\to {F}\left({A}\right)=\varnothing$
6 4 5 eqtr4d ${⊢}¬{A}\in \mathrm{V}\to \left({{F}↾}_{\left\{{A}\right\}}\right)\left({A}\right)={F}\left({A}\right)$
7 3 6 pm2.61i ${⊢}\left({{F}↾}_{\left\{{A}\right\}}\right)\left({A}\right)={F}\left({A}\right)$
8 funfv ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left({{F}↾}_{\left\{{A}\right\}}\right)\left({A}\right)=\bigcup \left({{F}↾}_{\left\{{A}\right\}}\right)\left[\left\{{A}\right\}\right]$
9 df-fun ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)↔\left(\mathrm{Rel}\left({{F}↾}_{\left\{{A}\right\}}\right)\wedge \left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\subseteq \mathrm{I}\right)$
10 9 simprbi ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\subseteq \mathrm{I}$
11 ssdif0 ${⊢}\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\subseteq \mathrm{I}↔\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}=\varnothing$
12 10 11 sylib ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}=\varnothing$
13 12 unieqd ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\bigcup \varnothing$
14 uni0 ${⊢}\bigcup \varnothing =\varnothing$
15 13 14 syl6eq ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$
16 15 unieqd ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\bigcup \varnothing$
17 16 14 syl6eq ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$
18 17 difeq2d ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to {F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)={F}\left[\left\{{A}\right\}\right]\setminus \varnothing$
19 resima ${⊢}\left({{F}↾}_{\left\{{A}\right\}}\right)\left[\left\{{A}\right\}\right]={F}\left[\left\{{A}\right\}\right]$
20 dif0 ${⊢}{F}\left[\left\{{A}\right\}\right]\setminus \varnothing ={F}\left[\left\{{A}\right\}\right]$
21 19 20 eqtr4i ${⊢}\left({{F}↾}_{\left\{{A}\right\}}\right)\left[\left\{{A}\right\}\right]={F}\left[\left\{{A}\right\}\right]\setminus \varnothing$
22 18 21 syl6reqr ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left({{F}↾}_{\left\{{A}\right\}}\right)\left[\left\{{A}\right\}\right]={F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
23 22 unieqd ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \bigcup \left({{F}↾}_{\left\{{A}\right\}}\right)\left[\left\{{A}\right\}\right]=\bigcup \left({F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$
24 8 23 eqtrd ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left({{F}↾}_{\left\{{A}\right\}}\right)\left({A}\right)=\bigcup \left({F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$
25 7 24 syl5eqr ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to {F}\left({A}\right)=\bigcup \left({F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$
26 nfunsn ${⊢}¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to {F}\left({A}\right)=\varnothing$
27 relres ${⊢}\mathrm{Rel}\left({{F}↾}_{\left\{{A}\right\}}\right)$
28 dffun3 ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)↔\left(\mathrm{Rel}\left({{F}↾}_{\left\{{A}\right\}}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {z}={y}\right)\right)$
29 27 28 mpbiran ${⊢}\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {z}={y}\right)$
30 iman ${⊢}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {z}={y}\right)↔¬\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
31 30 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {z}={y}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}¬\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
32 alnex ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}¬\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)↔¬\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
33 31 32 bitri ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {z}={y}\right)↔¬\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
34 33 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {z}={y}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}¬\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
35 exnal ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}¬\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)↔¬\forall {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
36 34 35 bitri ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {z}={y}\right)↔¬\forall {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
37 36 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {z}={y}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
38 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)↔¬\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
39 29 37 38 3bitrri ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)↔\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)$
40 39 con1bii ${⊢}¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
41 sp ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
42 41 eximi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
43 40 42 sylbi ${⊢}¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
44 snssi ${⊢}{A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left\{{A}\right\}\subseteq \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)$
45 residm ${⊢}{\left({{F}↾}_{\left\{{A}\right\}}\right)↾}_{\left\{{A}\right\}}={{F}↾}_{\left\{{A}\right\}}$
46 45 dmeqi ${⊢}\mathrm{dom}\left({\left({{F}↾}_{\left\{{A}\right\}}\right)↾}_{\left\{{A}\right\}}\right)=\mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)$
47 ssdmres ${⊢}\left\{{A}\right\}\subseteq \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)↔\mathrm{dom}\left({\left({{F}↾}_{\left\{{A}\right\}}\right)↾}_{\left\{{A}\right\}}\right)=\left\{{A}\right\}$
48 47 biimpi ${⊢}\left\{{A}\right\}\subseteq \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \mathrm{dom}\left({\left({{F}↾}_{\left\{{A}\right\}}\right)↾}_{\left\{{A}\right\}}\right)=\left\{{A}\right\}$
49 46 48 syl5eqr ${⊢}\left\{{A}\right\}\subseteq \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)=\left\{{A}\right\}$
50 44 49 syl ${⊢}{A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)=\left\{{A}\right\}$
51 vex ${⊢}{x}\in \mathrm{V}$
52 vex ${⊢}{z}\in \mathrm{V}$
53 51 52 breldm ${⊢}{x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {x}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)$
54 eleq2 ${⊢}\mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)=\left\{{A}\right\}\to \left({x}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)↔{x}\in \left\{{A}\right\}\right)$
55 velsn ${⊢}{x}\in \left\{{A}\right\}↔{x}={A}$
56 54 55 syl6bb ${⊢}\mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)=\left\{{A}\right\}\to \left({x}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)↔{x}={A}\right)$
57 56 biimpa ${⊢}\left(\mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)=\left\{{A}\right\}\wedge {x}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\right)\to {x}={A}$
58 50 53 57 syl2an ${⊢}\left({A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\to {x}={A}$
59 58 breq1d ${⊢}\left({A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\to \left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}↔{A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)$
60 59 biimpd ${⊢}\left({A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\to \left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)$
61 60 ex ${⊢}{A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to \left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\right)$
62 61 pm2.43d ${⊢}{A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)$
63 62 anim1d ${⊢}{A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left(\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\to \left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\right)$
64 63 eximdv ${⊢}{A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\right)$
65 64 exlimdv ${⊢}{A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\right)$
66 43 65 mpan9 ${⊢}\left(¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\wedge {A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)$
67 19 eleq2i ${⊢}{y}\in \left({{F}↾}_{\left\{{A}\right\}}\right)\left[\left\{{A}\right\}\right]↔{y}\in {F}\left[\left\{{A}\right\}\right]$
68 elimasni ${⊢}{y}\in \left({{F}↾}_{\left\{{A}\right\}}\right)\left[\left\{{A}\right\}\right]\to {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}$
69 67 68 sylbir ${⊢}{y}\in {F}\left[\left\{{A}\right\}\right]\to {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}$
70 vex ${⊢}{y}\in \mathrm{V}$
71 70 52 uniop ${⊢}\bigcup ⟨{y},{z}⟩=\left\{{y},{z}\right\}$
72 opex ${⊢}⟨{y},{z}⟩\in \mathrm{V}$
73 72 unisn ${⊢}\bigcup \left\{⟨{y},{z}⟩\right\}=⟨{y},{z}⟩$
74 27 brrelex1i ${⊢}{A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to {A}\in \mathrm{V}$
75 brcnvg ${⊢}\left({y}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to \left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{A}↔{A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)$
76 70 74 75 sylancr ${⊢}{A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\to \left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{A}↔{A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)$
77 76 biimpar ${⊢}\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)\to {y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{A}$
78 74 adantl ${⊢}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{A}\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\to {A}\in \mathrm{V}$
79 breq2 ${⊢}{x}={A}\to \left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}↔{y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{A}\right)$
80 breq1 ${⊢}{x}={A}\to \left({x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}↔{A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)$
81 79 80 anbi12d ${⊢}{x}={A}\to \left(\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)↔\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{A}\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\right)$
82 81 rspcev ${⊢}\left({A}\in \mathrm{V}\wedge \left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{A}\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\right)\to \exists {x}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)$
83 78 82 mpancom ${⊢}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{A}\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\to \exists {x}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)$
84 83 ancoms ${⊢}\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge {y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{A}\right)\to \exists {x}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)$
85 77 84 syldan ${⊢}\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)\to \exists {x}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)$
86 85 anim1i ${⊢}\left(\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)\wedge ¬{z}={y}\right)\to \left(\exists {x}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\wedge ¬{z}={y}\right)$
87 86 an32s ${⊢}\left(\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)\to \left(\exists {x}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\wedge ¬{z}={y}\right)$
88 eldif ${⊢}⟨{y},{z}⟩\in \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)↔\left(⟨{y},{z}⟩\in \left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\wedge ¬⟨{y},{z}⟩\in \mathrm{I}\right)$
89 rexv ${⊢}\exists {x}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)$
90 70 52 brco ${⊢}{y}\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right){z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)$
91 df-br ${⊢}{y}\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right){z}↔⟨{y},{z}⟩\in \left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)$
92 89 90 91 3bitr2ri ${⊢}⟨{y},{z}⟩\in \left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)↔\exists {x}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)$
93 52 ideq ${⊢}{y}\mathrm{I}{z}↔{y}={z}$
94 df-br ${⊢}{y}\mathrm{I}{z}↔⟨{y},{z}⟩\in \mathrm{I}$
95 equcom ${⊢}{y}={z}↔{z}={y}$
96 93 94 95 3bitr3i ${⊢}⟨{y},{z}⟩\in \mathrm{I}↔{z}={y}$
97 96 notbii ${⊢}¬⟨{y},{z}⟩\in \mathrm{I}↔¬{z}={y}$
98 92 97 anbi12i ${⊢}\left(⟨{y},{z}⟩\in \left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\wedge ¬⟨{y},{z}⟩\in \mathrm{I}\right)↔\left(\exists {x}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\wedge ¬{z}={y}\right)$
99 88 98 bitr2i ${⊢}\left(\exists {x}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\left({y}{\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}{x}\wedge {x}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\right)\wedge ¬{z}={y}\right)↔⟨{y},{z}⟩\in \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
100 87 99 sylib ${⊢}\left(\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)\to ⟨{y},{z}⟩\in \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
101 snssi ${⊢}⟨{y},{z}⟩\in \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\to \left\{⟨{y},{z}⟩\right\}\subseteq \left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}$
102 uniss ${⊢}\left\{⟨{y},{z}⟩\right\}\subseteq \left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\to \bigcup \left\{⟨{y},{z}⟩\right\}\subseteq \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
103 100 101 102 3syl ${⊢}\left(\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)\to \bigcup \left\{⟨{y},{z}⟩\right\}\subseteq \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
104 73 103 eqsstrrid ${⊢}\left(\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)\to ⟨{y},{z}⟩\subseteq \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
105 104 unissd ${⊢}\left(\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)\to \bigcup ⟨{y},{z}⟩\subseteq \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
106 71 105 eqsstrrid ${⊢}\left(\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)\to \left\{{y},{z}\right\}\subseteq \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
107 70 52 prss ${⊢}\left({y}\in \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\wedge {z}\in \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)↔\left\{{y},{z}\right\}\subseteq \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
108 106 107 sylibr ${⊢}\left(\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)\to \left({y}\in \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\wedge {z}\in \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$
109 108 simpld ${⊢}\left(\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\wedge {A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\right)\to {y}\in \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
110 109 ex ${⊢}\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\to \left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){y}\to {y}\in \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$
111 69 110 syl5 ${⊢}\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\to \left({y}\in {F}\left[\left\{{A}\right\}\right]\to {y}\in \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$
112 111 exlimiv ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({A}\left({{F}↾}_{\left\{{A}\right\}}\right){z}\wedge ¬{z}={y}\right)\to \left({y}\in {F}\left[\left\{{A}\right\}\right]\to {y}\in \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$
113 66 112 syl ${⊢}\left(¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\wedge {A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\right)\to \left({y}\in {F}\left[\left\{{A}\right\}\right]\to {y}\in \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$
114 113 ssrdv ${⊢}\left(¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\wedge {A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\right)\to {F}\left[\left\{{A}\right\}\right]\subseteq \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
115 ssdif0 ${⊢}{F}\left[\left\{{A}\right\}\right]\subseteq \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)↔{F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$
116 114 115 sylib ${⊢}\left(¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\wedge {A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\right)\to {F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$
117 116 ex ${⊢}¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left({A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to {F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing \right)$
118 ndmima ${⊢}¬{A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \left({{F}↾}_{\left\{{A}\right\}}\right)\left[\left\{{A}\right\}\right]=\varnothing$
119 19 118 syl5eqr ${⊢}¬{A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to {F}\left[\left\{{A}\right\}\right]=\varnothing$
120 119 difeq1d ${⊢}¬{A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to {F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing \setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)$
121 0dif ${⊢}\varnothing \setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$
122 120 121 syl6eq ${⊢}¬{A}\in \mathrm{dom}\left({{F}↾}_{\left\{{A}\right\}}\right)\to {F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$
123 117 122 pm2.61d1 ${⊢}¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to {F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)=\varnothing$
124 123 unieqd ${⊢}¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \bigcup \left({F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)=\bigcup \varnothing$
125 124 14 syl6eq ${⊢}¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to \bigcup \left({F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)=\varnothing$
126 26 125 eqtr4d ${⊢}¬\mathrm{Fun}\left({{F}↾}_{\left\{{A}\right\}}\right)\to {F}\left({A}\right)=\bigcup \left({F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$
127 25 126 pm2.61i ${⊢}{F}\left({A}\right)=\bigcup \left({F}\left[\left\{{A}\right\}\right]\setminus \bigcup \bigcup \left(\left(\left({{F}↾}_{\left\{{A}\right\}}\right)\circ {\left({{F}↾}_{\left\{{A}\right\}}\right)}^{-1}\right)\setminus \mathrm{I}\right)\right)$