Metamath Proof Explorer


Theorem bnj66

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj66.1 B = d | d A x d pred x A R d
bnj66.2 Y = x f pred x A R
bnj66.3 C = f | d B f Fn d x d f x = G Y
Assertion bnj66 g C Rel g

Proof

Step Hyp Ref Expression
1 bnj66.1 B = d | d A x d pred x A R d
2 bnj66.2 Y = x f pred x A R
3 bnj66.3 C = f | d B f Fn d x d f x = G Y
4 fneq1 g = f g Fn d f Fn d
5 fveq1 g = f g x = f x
6 reseq1 g = f g pred x A R = f pred x A R
7 6 opeq2d g = f x g pred x A R = x f pred x A R
8 7 2 eqtr4di g = f x g pred x A R = Y
9 8 fveq2d g = f G x g pred x A R = G Y
10 5 9 eqeq12d g = f g x = G x g pred x A R f x = G Y
11 10 ralbidv g = f x d g x = G x g pred x A R x d f x = G Y
12 4 11 anbi12d g = f g Fn d x d g x = G x g pred x A R f Fn d x d f x = G Y
13 12 rexbidv g = f d B g Fn d x d g x = G x g pred x A R d B f Fn d x d f x = G Y
14 13 cbvabv g | d B g Fn d x d g x = G x g pred x A R = f | d B f Fn d x d f x = G Y
15 3 14 eqtr4i C = g | d B g Fn d x d g x = G x g pred x A R
16 15 bnj1436 g C d B g Fn d x d g x = G x g pred x A R
17 bnj1239 d B g Fn d x d g x = G x g pred x A R d B g Fn d
18 fnrel g Fn d Rel g
19 18 rexlimivw d B g Fn d Rel g
20 16 17 19 3syl g C Rel g