Metamath Proof Explorer


Theorem bnj1442

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 bnj1442.1 B = d | d A x d pred x A R d
bnj1442.2 Y = x f pred x A R
bnj1442.3 C = f | d B f Fn d x d f x = G Y
bnj1442.4 τ f C dom f = x trCl x A R
bnj1442.5 D = x A | ¬ f τ
bnj1442.6 ψ R FrSe A D
bnj1442.7 χ ψ x D y D ¬ y R x
bnj1442.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1442.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
bnj1442.10 P = H
bnj1442.11 Z = x P pred x A R
bnj1442.12 Q = P x G Z
bnj1442.13 W = z Q pred z A R
bnj1442.14 E = x trCl x A R
bnj1442.15 χ P Fn trCl x A R
bnj1442.16 χ Q Fn x trCl x A R
bnj1442.17 θ χ z E
bnj1442.18 η θ z x
Assertion bnj1442 η Q z = G W

Proof

Step Hyp Ref Expression
1 bnj1442.1 B = d | d A x d pred x A R d
2 bnj1442.2 Y = x f pred x A R
3 bnj1442.3 C = f | d B f Fn d x d f x = G Y
4 bnj1442.4 τ f C dom f = x trCl x A R
5 bnj1442.5 D = x A | ¬ f τ
6 bnj1442.6 ψ R FrSe A D
7 bnj1442.7 χ ψ x D y D ¬ y R x
8 bnj1442.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1442.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 bnj1442.10 P = H
11 bnj1442.11 Z = x P pred x A R
12 bnj1442.12 Q = P x G Z
13 bnj1442.13 W = z Q pred z A R
14 bnj1442.14 E = x trCl x A R
15 bnj1442.15 χ P Fn trCl x A R
16 bnj1442.16 χ Q Fn x trCl x A R
17 bnj1442.17 θ χ z E
18 bnj1442.18 η θ z x
19 16 fnfund χ Fun Q
20 opex x G Z V
21 20 snid x G Z x G Z
22 elun2 x G Z x G Z x G Z P x G Z
23 21 22 ax-mp x G Z P x G Z
24 23 12 eleqtrri x G Z Q
25 funopfv Fun Q x G Z Q Q x = G Z
26 19 24 25 mpisyl χ Q x = G Z
27 17 26 bnj832 θ Q x = G Z
28 18 27 bnj832 η Q x = G Z
29 elsni z x z = x
30 18 29 simplbiim η z = x
31 30 fveq2d η Q z = Q x
32 bnj602 z = x pred z A R = pred x A R
33 32 reseq2d z = x Q pred z A R = Q pred x A R
34 30 33 syl η Q pred z A R = Q pred x A R
35 12 bnj931 P Q
36 35 a1i χ P Q
37 6 simplbi ψ R FrSe A
38 7 37 bnj835 χ R FrSe A
39 5 7 bnj1212 χ x A
40 bnj906 R FrSe A x A pred x A R trCl x A R
41 38 39 40 syl2anc χ pred x A R trCl x A R
42 15 fndmd χ dom P = trCl x A R
43 41 42 sseqtrrd χ pred x A R dom P
44 19 36 43 bnj1503 χ Q pred x A R = P pred x A R
45 17 44 bnj832 θ Q pred x A R = P pred x A R
46 18 45 bnj832 η Q pred x A R = P pred x A R
47 34 46 eqtrd η Q pred z A R = P pred x A R
48 30 47 opeq12d η z Q pred z A R = x P pred x A R
49 48 13 11 3eqtr4g η W = Z
50 49 fveq2d η G W = G Z
51 28 31 50 3eqtr4d η Q z = G W