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 φfAFunf
bnj1379.2 D=domfdomg
bnj1379.3 ψφfAgAfD=gD
bnj1379.5 χψxyAxzA
bnj1379.6 θχfAxyf
bnj1379.7 τθgAxzg
Assertion bnj1379 ψFunA

Proof

Step Hyp Ref Expression
1 bnj1379.1 φfAFunf
2 bnj1379.2 D=domfdomg
3 bnj1379.3 ψφfAgAfD=gD
4 bnj1379.5 χψxyAxzA
5 bnj1379.6 θχfAxyf
6 bnj1379.7 τθgAxzg
7 1 bnj1095 φfφ
8 7 nf5i fφ
9 nfra1 ffAgAfD=gD
10 8 9 nfan fφfAgAfD=gD
11 3 10 nfxfr fψ
12 1 bnj946 φffAFunf
13 12 biimpi φffAFunf
14 13 19.21bi φfAFunf
15 3 14 bnj832 ψfAFunf
16 funrel FunfRelf
17 15 16 syl6 ψfARelf
18 11 17 ralrimi ψfARelf
19 reluni RelAfARelf
20 18 19 sylibr ψRelA
21 eluni2 xyAfAxyf
22 21 biimpi xyAfAxyf
23 22 bnj1196 xyAffAxyf
24 4 23 bnj836 χffAxyf
25 nfv fxyA
26 nfv fxzA
27 11 25 26 nf3an fψxyAxzA
28 4 27 nfxfr fχ
29 28 nf5ri χfχ
30 24 5 29 bnj1345 χfθ
31 4 simp3bi χxzA
32 5 31 bnj835 θxzA
33 eluni2 xzAgAxzg
34 33 biimpi xzAgAxzg
35 34 bnj1196 xzAggAxzg
36 32 35 syl θggAxzg
37 nfv gφ
38 nfra2w gfAgAfD=gD
39 37 38 nfan gφfAgAfD=gD
40 3 39 nfxfr gψ
41 nfv gxyA
42 nfv gxzA
43 40 41 42 nf3an gψxyAxzA
44 4 43 nfxfr gχ
45 nfv gfA
46 nfv gxyf
47 44 45 46 nf3an gχfAxyf
48 5 47 nfxfr gθ
49 48 nf5ri θgθ
50 36 6 49 bnj1345 θgτ
51 3 simprbi ψfAgAfD=gD
52 4 51 bnj835 χfAgAfD=gD
53 5 52 bnj835 θfAgAfD=gD
54 6 53 bnj835 τfAgAfD=gD
55 5 6 bnj1219 τfA
56 54 55 bnj1294 τgAfD=gD
57 6 simp2bi τgA
58 56 57 bnj1294 τfD=gD
59 58 fveq1d τfDx=gDx
60 5 simp3bi θxyf
61 6 60 bnj835 τxyf
62 vex xV
63 vex yV
64 62 63 opeldm xyfxdomf
65 61 64 syl τxdomf
66 vex zV
67 62 66 opeldm xzgxdomg
68 6 67 bnj837 τxdomg
69 65 68 elind τxdomfdomg
70 69 2 eleqtrrdi τxD
71 70 fvresd τfDx=fx
72 70 fvresd τgDx=gx
73 59 71 72 3eqtr3d τfx=gx
74 1 biimpi φfAFunf
75 3 74 bnj832 ψfAFunf
76 4 75 bnj835 χfAFunf
77 5 76 bnj835 θfAFunf
78 6 77 bnj835 τfAFunf
79 78 55 bnj1294 τFunf
80 funopfv Funfxyffx=y
81 79 61 80 sylc τfx=y
82 funeq f=gFunfFung
83 82 78 57 rspcdva τFung
84 6 simp3bi τxzg
85 funopfv Fungxzggx=z
86 83 84 85 sylc τgx=z
87 73 81 86 3eqtr3d τy=z
88 50 87 bnj593 θgy=z
89 88 bnj937 θy=z
90 30 89 bnj593 χfy=z
91 90 bnj937 χy=z
92 4 91 sylbir ψxyAxzAy=z
93 92 3expib ψxyAxzAy=z
94 93 alrimivv ψyzxyAxzAy=z
95 94 alrimiv ψxyzxyAxzAy=z
96 dffun4 FunARelAxyzxyAxzAy=z
97 20 95 96 sylanbrc ψFunA