Metamath Proof Explorer


Theorem bnj1447

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 bnj1447.1 B=d|dAxdpredxARd
bnj1447.2 Y=xfpredxAR
bnj1447.3 C=f|dBfFndxdfx=GY
bnj1447.4 τfCdomf=xtrClxAR
bnj1447.5 D=xA|¬fτ
bnj1447.6 ψRFrSeAD
bnj1447.7 χψxDyD¬yRx
bnj1447.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1447.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
bnj1447.10 P=H
bnj1447.11 Z=xPpredxAR
bnj1447.12 Q=PxGZ
bnj1447.13 W=zQpredzAR
Assertion bnj1447 Qz=GWyQz=GW

Proof

Step Hyp Ref Expression
1 bnj1447.1 B=d|dAxdpredxARd
2 bnj1447.2 Y=xfpredxAR
3 bnj1447.3 C=f|dBfFndxdfx=GY
4 bnj1447.4 τfCdomf=xtrClxAR
5 bnj1447.5 D=xA|¬fτ
6 bnj1447.6 ψRFrSeAD
7 bnj1447.7 χψxDyD¬yRx
8 bnj1447.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1447.9 Could not format H = { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
10 bnj1447.10 P=H
11 bnj1447.11 Z=xPpredxAR
12 bnj1447.12 Q=PxGZ
13 bnj1447.13 W=zQpredzAR
14 nfre1 Could not format F/ y E. y e. _pred ( x , A , R ) ta' : No typesetting found for |- F/ y E. y e. _pred ( x , A , R ) ta' with typecode |-
15 14 nfab Could not format F/_ y { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- F/_ y { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
16 9 15 nfcxfr _yH
17 16 nfuni _yH
18 10 17 nfcxfr _yP
19 nfcv _yx
20 nfcv _yG
21 nfcv _ypredxAR
22 18 21 nfres _yPpredxAR
23 19 22 nfop _yxPpredxAR
24 11 23 nfcxfr _yZ
25 20 24 nffv _yGZ
26 19 25 nfop _yxGZ
27 26 nfsn _yxGZ
28 18 27 nfun _yPxGZ
29 12 28 nfcxfr _yQ
30 nfcv _yz
31 29 30 nffv _yQz
32 nfcv _ypredzAR
33 29 32 nfres _yQpredzAR
34 30 33 nfop _yzQpredzAR
35 13 34 nfcxfr _yW
36 20 35 nffv _yGW
37 31 36 nfeq yQz=GW
38 37 nf5ri Qz=GWyQz=GW