Metamath Proof Explorer

Theorem fpwrelmapffslem

Description: Lemma for fpwrelmapffs . For this theorem, the sets A and B could be infinite, but the relation R itself is finite. (Contributed by Thierry Arnoux, 1-Sep-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses fpwrelmapffslem.1 ${⊢}{A}\in \mathrm{V}$
fpwrelmapffslem.2 ${⊢}{B}\in \mathrm{V}$
fpwrelmapffslem.3 ${⊢}{\phi }\to {F}:{A}⟶𝒫{B}$
fpwrelmapffslem.4 ${⊢}{\phi }\to {R}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}$
Assertion fpwrelmapffslem ${⊢}{\phi }\to \left({R}\in \mathrm{Fin}↔\left(\mathrm{ran}{F}\subseteq \mathrm{Fin}\wedge {F}\mathrm{supp}\varnothing \in \mathrm{Fin}\right)\right)$

Proof

Step Hyp Ref Expression
1 fpwrelmapffslem.1 ${⊢}{A}\in \mathrm{V}$
2 fpwrelmapffslem.2 ${⊢}{B}\in \mathrm{V}$
3 fpwrelmapffslem.3 ${⊢}{\phi }\to {F}:{A}⟶𝒫{B}$
4 fpwrelmapffslem.4 ${⊢}{\phi }\to {R}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}$
5 relopab ${⊢}\mathrm{Rel}\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}$
6 releq ${⊢}{R}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}\to \left(\mathrm{Rel}{R}↔\mathrm{Rel}\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}\right)$
7 5 6 mpbiri ${⊢}{R}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}\to \mathrm{Rel}{R}$
8 relfi ${⊢}\mathrm{Rel}{R}\to \left({R}\in \mathrm{Fin}↔\left(\mathrm{dom}{R}\in \mathrm{Fin}\wedge \mathrm{ran}{R}\in \mathrm{Fin}\right)\right)$
9 4 7 8 3syl ${⊢}{\phi }\to \left({R}\in \mathrm{Fin}↔\left(\mathrm{dom}{R}\in \mathrm{Fin}\wedge \mathrm{ran}{R}\in \mathrm{Fin}\right)\right)$
10 rexcom4 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}={F}\left({x}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}={F}\left({x}\right)\right)$
11 ancom ${⊢}\left({z}={F}\left({x}\right)\wedge {w}\in {z}\right)↔\left({w}\in {z}\wedge {z}={F}\left({x}\right)\right)$
12 11 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}={F}\left({x}\right)\wedge {w}\in {z}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}={F}\left({x}\right)\right)$
13 fvex ${⊢}{F}\left({x}\right)\in \mathrm{V}$
14 eleq2 ${⊢}{z}={F}\left({x}\right)\to \left({w}\in {z}↔{w}\in {F}\left({x}\right)\right)$
15 13 14 ceqsexv ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}={F}\left({x}\right)\wedge {w}\in {z}\right)↔{w}\in {F}\left({x}\right)$
16 12 15 bitr3i ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}={F}\left({x}\right)\right)↔{w}\in {F}\left({x}\right)$
17 16 rexbii ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}={F}\left({x}\right)\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{w}\in {F}\left({x}\right)$
18 r19.42v ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}={F}\left({x}\right)\right)↔\left({w}\in {z}\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right)$
19 18 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge {z}={F}\left({x}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right)$
20 10 17 19 3bitr3ri ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{w}\in {F}\left({x}\right)$
21 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{w}\in {F}\left({x}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {w}\in {F}\left({x}\right)\right)$
22 20 21 bitr2i ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {w}\in {F}\left({x}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right)$
23 22 a1i ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {w}\in {F}\left({x}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right)\right)$
24 vex ${⊢}{w}\in \mathrm{V}$
25 eleq1w ${⊢}{y}={w}\to \left({y}\in {F}\left({x}\right)↔{w}\in {F}\left({x}\right)\right)$
26 25 anbi2d ${⊢}{y}={w}\to \left(\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)↔\left({x}\in {A}\wedge {w}\in {F}\left({x}\right)\right)\right)$
27 26 exbidv ${⊢}{y}={w}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {w}\in {F}\left({x}\right)\right)\right)$
28 24 27 elab ${⊢}{w}\in \left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {w}\in {F}\left({x}\right)\right)$
29 eluniab ${⊢}{w}\in \bigcup \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right)$
30 23 28 29 3bitr4g ${⊢}{\phi }\to \left({w}\in \left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}↔{w}\in \bigcup \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\right)$
31 30 eqrdv ${⊢}{\phi }\to \left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}=\bigcup \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}$
32 31 eleq1d ${⊢}{\phi }\to \left(\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}\in \mathrm{Fin}↔\bigcup \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\in \mathrm{Fin}\right)$
33 32 adantr ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \left(\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}\in \mathrm{Fin}↔\bigcup \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\in \mathrm{Fin}\right)$
34 ffn ${⊢}{F}:{A}⟶𝒫{B}\to {F}Fn{A}$
35 fnrnfv ${⊢}{F}Fn{A}\to \mathrm{ran}{F}=\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}$
36 3 34 35 3syl ${⊢}{\phi }\to \mathrm{ran}{F}=\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}$
37 36 adantr ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \mathrm{ran}{F}=\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}$
38 0ex ${⊢}\varnothing \in \mathrm{V}$
39 38 a1i ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \varnothing \in \mathrm{V}$
40 fex ${⊢}\left({F}:{A}⟶𝒫{B}\wedge {A}\in \mathrm{V}\right)\to {F}\in \mathrm{V}$
41 3 1 40 sylancl ${⊢}{\phi }\to {F}\in \mathrm{V}$
42 41 adantr ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to {F}\in \mathrm{V}$
43 3 ffund ${⊢}{\phi }\to \mathrm{Fun}{F}$
44 43 adantr ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \mathrm{Fun}{F}$
45 opabdm ${⊢}{R}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}\to \mathrm{dom}{R}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}$
46 4 45 syl ${⊢}{\phi }\to \mathrm{dom}{R}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}$
47 1 40 mpan2 ${⊢}{F}:{A}⟶𝒫{B}\to {F}\in \mathrm{V}$
48 suppimacnv ${⊢}\left({F}\in \mathrm{V}\wedge \varnothing \in \mathrm{V}\right)\to {F}\mathrm{supp}\varnothing ={{F}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]$
49 38 48 mpan2 ${⊢}{F}\in \mathrm{V}\to {F}\mathrm{supp}\varnothing ={{F}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]$
50 3 47 49 3syl ${⊢}{\phi }\to {F}\mathrm{supp}\varnothing ={{F}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]$
51 3 feqmptd ${⊢}{\phi }\to {F}=\left({x}\in {A}⟼{F}\left({x}\right)\right)$
52 51 cnveqd ${⊢}{\phi }\to {{F}}^{-1}={\left({x}\in {A}⟼{F}\left({x}\right)\right)}^{-1}$
53 52 imaeq1d ${⊢}{\phi }\to {{F}}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]={\left({x}\in {A}⟼{F}\left({x}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]$
54 50 53 eqtrd ${⊢}{\phi }\to {F}\mathrm{supp}\varnothing ={\left({x}\in {A}⟼{F}\left({x}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]$
55 eqid ${⊢}\left({x}\in {A}⟼{F}\left({x}\right)\right)=\left({x}\in {A}⟼{F}\left({x}\right)\right)$
56 55 mptpreima ${⊢}{\left({x}\in {A}⟼{F}\left({x}\right)\right)}^{-1}\left[\mathrm{V}\setminus \left\{\varnothing \right\}\right]=\left\{{x}\in {A}|{F}\left({x}\right)\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)\right\}$
57 54 56 syl6eq ${⊢}{\phi }\to {F}\mathrm{supp}\varnothing =\left\{{x}\in {A}|{F}\left({x}\right)\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)\right\}$
58 suppvalfn ${⊢}\left({F}Fn{A}\wedge {A}\in \mathrm{V}\wedge \varnothing \in \mathrm{V}\right)\to {F}\mathrm{supp}\varnothing =\left\{{x}\in {A}|{F}\left({x}\right)\ne \varnothing \right\}$
59 1 38 58 mp3an23 ${⊢}{F}Fn{A}\to {F}\mathrm{supp}\varnothing =\left\{{x}\in {A}|{F}\left({x}\right)\ne \varnothing \right\}$
60 3 34 59 3syl ${⊢}{\phi }\to {F}\mathrm{supp}\varnothing =\left\{{x}\in {A}|{F}\left({x}\right)\ne \varnothing \right\}$
61 n0 ${⊢}{F}\left({x}\right)\ne \varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {F}\left({x}\right)$
62 61 rabbii ${⊢}\left\{{x}\in {A}|{F}\left({x}\right)\ne \varnothing \right\}=\left\{{x}\in {A}|\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {F}\left({x}\right)\right\}$
63 62 a1i ${⊢}{\phi }\to \left\{{x}\in {A}|{F}\left({x}\right)\ne \varnothing \right\}=\left\{{x}\in {A}|\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {F}\left({x}\right)\right\}$
64 60 57 63 3eqtr3d ${⊢}{\phi }\to \left\{{x}\in {A}|{F}\left({x}\right)\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)\right\}=\left\{{x}\in {A}|\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {F}\left({x}\right)\right\}$
65 df-rab ${⊢}\left\{{x}\in {A}|\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {F}\left({x}\right)\right\}=\left\{{x}|\left({x}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {F}\left({x}\right)\right)\right\}$
66 19.42v ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)↔\left({x}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {F}\left({x}\right)\right)$
67 66 abbii ${⊢}\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}=\left\{{x}|\left({x}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {F}\left({x}\right)\right)\right\}$
68 65 67 eqtr4i ${⊢}\left\{{x}\in {A}|\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {F}\left({x}\right)\right\}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}$
69 68 a1i ${⊢}{\phi }\to \left\{{x}\in {A}|\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {F}\left({x}\right)\right\}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}$
70 57 64 69 3eqtrd ${⊢}{\phi }\to {F}\mathrm{supp}\varnothing =\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}$
71 46 70 eqtr4d ${⊢}{\phi }\to \mathrm{dom}{R}={F}\mathrm{supp}\varnothing$
72 71 eleq1d ${⊢}{\phi }\to \left(\mathrm{dom}{R}\in \mathrm{Fin}↔{F}\mathrm{supp}\varnothing \in \mathrm{Fin}\right)$
73 72 biimpa ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to {F}\mathrm{supp}\varnothing \in \mathrm{Fin}$
74 39 42 44 73 ffsrn ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \mathrm{ran}{F}\in \mathrm{Fin}$
75 37 74 eqeltrrd ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\in \mathrm{Fin}$
76 unifi ${⊢}\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\in \mathrm{Fin}\wedge \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\subseteq \mathrm{Fin}\right)\to \bigcup \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\in \mathrm{Fin}$
77 76 ex ${⊢}\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\in \mathrm{Fin}\to \left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\subseteq \mathrm{Fin}\to \bigcup \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\in \mathrm{Fin}\right)$
78 75 77 syl ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\subseteq \mathrm{Fin}\to \bigcup \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\in \mathrm{Fin}\right)$
79 unifi3 ${⊢}\bigcup \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\in \mathrm{Fin}\to \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\subseteq \mathrm{Fin}$
80 78 79 impbid1 ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\subseteq \mathrm{Fin}↔\bigcup \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\in \mathrm{Fin}\right)$
81 33 80 bitr4d ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \left(\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}\in \mathrm{Fin}↔\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\subseteq \mathrm{Fin}\right)$
82 opabrn ${⊢}{R}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}\to \mathrm{ran}{R}=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}$
83 4 82 syl ${⊢}{\phi }\to \mathrm{ran}{R}=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}$
84 83 eleq1d ${⊢}{\phi }\to \left(\mathrm{ran}{R}\in \mathrm{Fin}↔\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}\in \mathrm{Fin}\right)$
85 84 adantr ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \left(\mathrm{ran}{R}\in \mathrm{Fin}↔\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in {F}\left({x}\right)\right)\right\}\in \mathrm{Fin}\right)$
86 37 sseq1d ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \left(\mathrm{ran}{F}\subseteq \mathrm{Fin}↔\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={F}\left({x}\right)\right\}\subseteq \mathrm{Fin}\right)$
87 81 85 86 3bitr4d ${⊢}\left({\phi }\wedge \mathrm{dom}{R}\in \mathrm{Fin}\right)\to \left(\mathrm{ran}{R}\in \mathrm{Fin}↔\mathrm{ran}{F}\subseteq \mathrm{Fin}\right)$
88 87 pm5.32da ${⊢}{\phi }\to \left(\left(\mathrm{dom}{R}\in \mathrm{Fin}\wedge \mathrm{ran}{R}\in \mathrm{Fin}\right)↔\left(\mathrm{dom}{R}\in \mathrm{Fin}\wedge \mathrm{ran}{F}\subseteq \mathrm{Fin}\right)\right)$
89 72 anbi1d ${⊢}{\phi }\to \left(\left(\mathrm{dom}{R}\in \mathrm{Fin}\wedge \mathrm{ran}{F}\subseteq \mathrm{Fin}\right)↔\left({F}\mathrm{supp}\varnothing \in \mathrm{Fin}\wedge \mathrm{ran}{F}\subseteq \mathrm{Fin}\right)\right)$
90 88 89 bitrd ${⊢}{\phi }\to \left(\left(\mathrm{dom}{R}\in \mathrm{Fin}\wedge \mathrm{ran}{R}\in \mathrm{Fin}\right)↔\left({F}\mathrm{supp}\varnothing \in \mathrm{Fin}\wedge \mathrm{ran}{F}\subseteq \mathrm{Fin}\right)\right)$
91 ancom ${⊢}\left({F}\mathrm{supp}\varnothing \in \mathrm{Fin}\wedge \mathrm{ran}{F}\subseteq \mathrm{Fin}\right)↔\left(\mathrm{ran}{F}\subseteq \mathrm{Fin}\wedge {F}\mathrm{supp}\varnothing \in \mathrm{Fin}\right)$
92 91 a1i ${⊢}{\phi }\to \left(\left({F}\mathrm{supp}\varnothing \in \mathrm{Fin}\wedge \mathrm{ran}{F}\subseteq \mathrm{Fin}\right)↔\left(\mathrm{ran}{F}\subseteq \mathrm{Fin}\wedge {F}\mathrm{supp}\varnothing \in \mathrm{Fin}\right)\right)$
93 9 90 92 3bitrd ${⊢}{\phi }\to \left({R}\in \mathrm{Fin}↔\left(\mathrm{ran}{F}\subseteq \mathrm{Fin}\wedge {F}\mathrm{supp}\varnothing \in \mathrm{Fin}\right)\right)$