# Metamath Proof Explorer

## Theorem bnj1379

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1379.1 ${⊢}{\phi }↔\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}$
bnj1379.2 ${⊢}{D}=\mathrm{dom}{f}\cap \mathrm{dom}{g}$
bnj1379.3 ${⊢}{\psi }↔\left({\phi }\wedge \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)$
bnj1379.5 ${⊢}{\chi }↔\left({\psi }\wedge ⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)$
bnj1379.6 ${⊢}{\theta }↔\left({\chi }\wedge {f}\in {A}\wedge ⟨{x},{y}⟩\in {f}\right)$
bnj1379.7 ${⊢}{\tau }↔\left({\theta }\wedge {g}\in {A}\wedge ⟨{x},{z}⟩\in {g}\right)$
Assertion bnj1379 ${⊢}{\psi }\to \mathrm{Fun}\bigcup {A}$

### Proof

Step Hyp Ref Expression
1 bnj1379.1 ${⊢}{\phi }↔\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}$
2 bnj1379.2 ${⊢}{D}=\mathrm{dom}{f}\cap \mathrm{dom}{g}$
3 bnj1379.3 ${⊢}{\psi }↔\left({\phi }\wedge \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)$
4 bnj1379.5 ${⊢}{\chi }↔\left({\psi }\wedge ⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)$
5 bnj1379.6 ${⊢}{\theta }↔\left({\chi }\wedge {f}\in {A}\wedge ⟨{x},{y}⟩\in {f}\right)$
6 bnj1379.7 ${⊢}{\tau }↔\left({\theta }\wedge {g}\in {A}\wedge ⟨{x},{z}⟩\in {g}\right)$
7 1 bnj1095 ${⊢}{\phi }\to \forall {f}\phantom{\rule{.4em}{0ex}}{\phi }$
8 7 nf5i ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}{\phi }$
9 nfra1 ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}$
10 8 9 nfan ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)$
11 3 10 nfxfr ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}{\psi }$
12 1 bnj946 ${⊢}{\phi }↔\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {A}\to \mathrm{Fun}{f}\right)$
13 12 biimpi ${⊢}{\phi }\to \forall {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {A}\to \mathrm{Fun}{f}\right)$
14 13 19.21bi ${⊢}{\phi }\to \left({f}\in {A}\to \mathrm{Fun}{f}\right)$
15 3 14 bnj832 ${⊢}{\psi }\to \left({f}\in {A}\to \mathrm{Fun}{f}\right)$
16 funrel ${⊢}\mathrm{Fun}{f}\to \mathrm{Rel}{f}$
17 15 16 syl6 ${⊢}{\psi }\to \left({f}\in {A}\to \mathrm{Rel}{f}\right)$
18 11 17 ralrimi ${⊢}{\psi }\to \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}{f}$
19 reluni ${⊢}\mathrm{Rel}\bigcup {A}↔\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}{f}$
20 18 19 sylibr ${⊢}{\psi }\to \mathrm{Rel}\bigcup {A}$
21 eluni2 ${⊢}⟨{x},{y}⟩\in \bigcup {A}↔\exists {f}\in {A}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {f}$
22 21 biimpi ${⊢}⟨{x},{y}⟩\in \bigcup {A}\to \exists {f}\in {A}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {f}$
23 22 bnj1196 ${⊢}⟨{x},{y}⟩\in \bigcup {A}\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {A}\wedge ⟨{x},{y}⟩\in {f}\right)$
24 4 23 bnj836 ${⊢}{\chi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {A}\wedge ⟨{x},{y}⟩\in {f}\right)$
25 nfv ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in \bigcup {A}$
26 nfv ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}⟨{x},{z}⟩\in \bigcup {A}$
27 11 25 26 nf3an ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)$
28 4 27 nfxfr ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}{\chi }$
29 28 nf5ri ${⊢}{\chi }\to \forall {f}\phantom{\rule{.4em}{0ex}}{\chi }$
30 24 5 29 bnj1345 ${⊢}{\chi }\to \exists {f}\phantom{\rule{.4em}{0ex}}{\theta }$
31 4 simp3bi ${⊢}{\chi }\to ⟨{x},{z}⟩\in \bigcup {A}$
32 5 31 bnj835 ${⊢}{\theta }\to ⟨{x},{z}⟩\in \bigcup {A}$
33 eluni2 ${⊢}⟨{x},{z}⟩\in \bigcup {A}↔\exists {g}\in {A}\phantom{\rule{.4em}{0ex}}⟨{x},{z}⟩\in {g}$
34 33 biimpi ${⊢}⟨{x},{z}⟩\in \bigcup {A}\to \exists {g}\in {A}\phantom{\rule{.4em}{0ex}}⟨{x},{z}⟩\in {g}$
35 34 bnj1196 ${⊢}⟨{x},{z}⟩\in \bigcup {A}\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}\in {A}\wedge ⟨{x},{z}⟩\in {g}\right)$
36 32 35 syl ${⊢}{\theta }\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}\in {A}\wedge ⟨{x},{z}⟩\in {g}\right)$
37 nfv ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}{\phi }$
38 nfra2w ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}$
39 37 38 nfan ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)$
40 3 39 nfxfr ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}{\psi }$
41 nfv ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in \bigcup {A}$
42 nfv ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}⟨{x},{z}⟩\in \bigcup {A}$
43 40 41 42 nf3an ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge ⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)$
44 4 43 nfxfr ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}{\chi }$
45 nfv ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}{f}\in {A}$
46 nfv ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {f}$
47 44 45 46 nf3an ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}\left({\chi }\wedge {f}\in {A}\wedge ⟨{x},{y}⟩\in {f}\right)$
48 5 47 nfxfr ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}{\theta }$
49 48 nf5ri ${⊢}{\theta }\to \forall {g}\phantom{\rule{.4em}{0ex}}{\theta }$
50 36 6 49 bnj1345 ${⊢}{\theta }\to \exists {g}\phantom{\rule{.4em}{0ex}}{\tau }$
51 3 simprbi ${⊢}{\psi }\to \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}$
52 4 51 bnj835 ${⊢}{\chi }\to \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}$
53 5 52 bnj835 ${⊢}{\theta }\to \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}$
54 6 53 bnj835 ${⊢}{\tau }\to \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}$
55 5 6 bnj1219 ${⊢}{\tau }\to {f}\in {A}$
56 54 55 bnj1294 ${⊢}{\tau }\to \forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}$
57 6 simp2bi ${⊢}{\tau }\to {g}\in {A}$
58 56 57 bnj1294 ${⊢}{\tau }\to {{f}↾}_{{D}}={{g}↾}_{{D}}$
59 58 fveq1d ${⊢}{\tau }\to \left({{f}↾}_{{D}}\right)\left({x}\right)=\left({{g}↾}_{{D}}\right)\left({x}\right)$
60 5 simp3bi ${⊢}{\theta }\to ⟨{x},{y}⟩\in {f}$
61 6 60 bnj835 ${⊢}{\tau }\to ⟨{x},{y}⟩\in {f}$
62 vex ${⊢}{x}\in \mathrm{V}$
63 vex ${⊢}{y}\in \mathrm{V}$
64 62 63 opeldm ${⊢}⟨{x},{y}⟩\in {f}\to {x}\in \mathrm{dom}{f}$
65 61 64 syl ${⊢}{\tau }\to {x}\in \mathrm{dom}{f}$
66 vex ${⊢}{z}\in \mathrm{V}$
67 62 66 opeldm ${⊢}⟨{x},{z}⟩\in {g}\to {x}\in \mathrm{dom}{g}$
68 6 67 bnj837 ${⊢}{\tau }\to {x}\in \mathrm{dom}{g}$
69 65 68 elind ${⊢}{\tau }\to {x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)$
70 69 2 eleqtrrdi ${⊢}{\tau }\to {x}\in {D}$
71 70 fvresd ${⊢}{\tau }\to \left({{f}↾}_{{D}}\right)\left({x}\right)={f}\left({x}\right)$
72 70 fvresd ${⊢}{\tau }\to \left({{g}↾}_{{D}}\right)\left({x}\right)={g}\left({x}\right)$
73 59 71 72 3eqtr3d ${⊢}{\tau }\to {f}\left({x}\right)={g}\left({x}\right)$
74 1 biimpi ${⊢}{\phi }\to \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}$
75 3 74 bnj832 ${⊢}{\psi }\to \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}$
76 4 75 bnj835 ${⊢}{\chi }\to \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}$
77 5 76 bnj835 ${⊢}{\theta }\to \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}$
78 6 77 bnj835 ${⊢}{\tau }\to \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}$
79 78 55 bnj1294 ${⊢}{\tau }\to \mathrm{Fun}{f}$
80 funopfv ${⊢}\mathrm{Fun}{f}\to \left(⟨{x},{y}⟩\in {f}\to {f}\left({x}\right)={y}\right)$
81 79 61 80 sylc ${⊢}{\tau }\to {f}\left({x}\right)={y}$
82 funeq ${⊢}{f}={g}\to \left(\mathrm{Fun}{f}↔\mathrm{Fun}{g}\right)$
83 82 78 57 rspcdva ${⊢}{\tau }\to \mathrm{Fun}{g}$
84 6 simp3bi ${⊢}{\tau }\to ⟨{x},{z}⟩\in {g}$
85 funopfv ${⊢}\mathrm{Fun}{g}\to \left(⟨{x},{z}⟩\in {g}\to {g}\left({x}\right)={z}\right)$
86 83 84 85 sylc ${⊢}{\tau }\to {g}\left({x}\right)={z}$
87 73 81 86 3eqtr3d ${⊢}{\tau }\to {y}={z}$
88 50 87 bnj593 ${⊢}{\theta }\to \exists {g}\phantom{\rule{.4em}{0ex}}{y}={z}$
89 88 bnj937 ${⊢}{\theta }\to {y}={z}$
90 30 89 bnj593 ${⊢}{\chi }\to \exists {f}\phantom{\rule{.4em}{0ex}}{y}={z}$
91 90 bnj937 ${⊢}{\chi }\to {y}={z}$
92 4 91 sylbir ${⊢}\left({\psi }\wedge ⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)\to {y}={z}$
93 92 3expib ${⊢}{\psi }\to \left(\left(⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)\to {y}={z}\right)$
94 93 alrimivv ${⊢}{\psi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)\to {y}={z}\right)$
95 94 alrimiv ${⊢}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)\to {y}={z}\right)$
96 dffun4 ${⊢}\mathrm{Fun}\bigcup {A}↔\left(\mathrm{Rel}\bigcup {A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in \bigcup {A}\wedge ⟨{x},{z}⟩\in \bigcup {A}\right)\to {y}={z}\right)\right)$
97 20 95 96 sylanbrc ${⊢}{\psi }\to \mathrm{Fun}\bigcup {A}$