Metamath Proof Explorer


Theorem bnj1280

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 bnj1280.1 B=d|dAxdpredxARd
bnj1280.2 Y=xfpredxAR
bnj1280.3 C=f|dBfFndxdfx=GY
bnj1280.4 D=domgdomh
bnj1280.5 E=xD|gxhx
bnj1280.6 φRFrSeAgChCgDhD
bnj1280.7 ψφxEyE¬yRx
bnj1280.17 ψpredxARE=
Assertion bnj1280 ψgpredxAR=hpredxAR

Proof

Step Hyp Ref Expression
1 bnj1280.1 B=d|dAxdpredxARd
2 bnj1280.2 Y=xfpredxAR
3 bnj1280.3 C=f|dBfFndxdfx=GY
4 bnj1280.4 D=domgdomh
5 bnj1280.5 E=xD|gxhx
6 bnj1280.6 φRFrSeAgChCgDhD
7 bnj1280.7 ψφxEyE¬yRx
8 bnj1280.17 ψpredxARE=
9 1 2 3 4 5 6 7 bnj1286 ψpredxARD
10 9 sseld ψzpredxARzD
11 disj1 predxARE=zzpredxAR¬zE
12 8 11 sylib ψzzpredxAR¬zE
13 12 19.21bi ψzpredxAR¬zE
14 fveq2 x=zgx=gz
15 fveq2 x=zhx=hz
16 14 15 neeq12d x=zgxhxgzhz
17 16 5 elrab2 zEzDgzhz
18 17 notbii ¬zE¬zDgzhz
19 imnan zD¬gzhz¬zDgzhz
20 nne ¬gzhzgz=hz
21 20 imbi2i zD¬gzhzzDgz=hz
22 18 19 21 3bitr2i ¬zEzDgz=hz
23 13 22 imbitrdi ψzpredxARzDgz=hz
24 10 23 mpdd ψzpredxARgz=hz
25 24 imp ψzpredxARgz=hz
26 fvres zDgDz=gz
27 10 26 syl6 ψzpredxARgDz=gz
28 27 imp ψzpredxARgDz=gz
29 fvres zDhDz=hz
30 10 29 syl6 ψzpredxARhDz=hz
31 30 imp ψzpredxARhDz=hz
32 25 28 31 3eqtr4d ψzpredxARgDz=hDz
33 32 ralrimiva ψzpredxARgDz=hDz
34 9 resabs1d ψgDpredxAR=gpredxAR
35 9 resabs1d ψhDpredxAR=hpredxAR
36 34 35 eqeq12d ψgDpredxAR=hDpredxARgpredxAR=hpredxAR
37 1 2 3 4 5 6 7 bnj1256 φdBgFnd
38 4 bnj1292 Ddomg
39 fndm gFnddomg=d
40 38 39 sseqtrid gFndDd
41 fnssres gFndDdgDFnD
42 40 41 mpdan gFndgDFnD
43 37 42 bnj31 φdBgDFnD
44 43 bnj1265 φgDFnD
45 7 44 bnj835 ψgDFnD
46 1 2 3 4 5 6 7 bnj1259 φdBhFnd
47 4 bnj1293 Ddomh
48 fndm hFnddomh=d
49 47 48 sseqtrid hFndDd
50 fnssres hFndDdhDFnD
51 49 50 mpdan hFndhDFnD
52 46 51 bnj31 φdBhDFnD
53 52 bnj1265 φhDFnD
54 7 53 bnj835 ψhDFnD
55 fvreseq gDFnDhDFnDpredxARDgDpredxAR=hDpredxARzpredxARgDz=hDz
56 45 54 9 55 syl21anc ψgDpredxAR=hDpredxARzpredxARgDz=hDz
57 36 56 bitr3d ψgpredxAR=hpredxARzpredxARgDz=hDz
58 33 57 mpbird ψgpredxAR=hpredxAR