Metamath Proof Explorer


Theorem bnj1145

Description: Technical lemma for bnj69 . 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 bnj1145.1 φ f = pred X A R
bnj1145.2 ψ i ω suc i n f suc i = y f i pred y A R
bnj1145.3 D = ω
bnj1145.4 B = f | n D f Fn n φ ψ
bnj1145.5 χ n D f Fn n φ ψ
bnj1145.6 θ i i n χ j n i = suc j
Assertion bnj1145 trCl X A R A

Proof

Step Hyp Ref Expression
1 bnj1145.1 φ f = pred X A R
2 bnj1145.2 ψ i ω suc i n f suc i = y f i pred y A R
3 bnj1145.3 D = ω
4 bnj1145.4 B = f | n D f Fn n φ ψ
5 bnj1145.5 χ n D f Fn n φ ψ
6 bnj1145.6 θ i i n χ j n i = suc j
7 1 2 3 4 bnj882 trCl X A R = f B i dom f f i
8 ss2iun f B i dom f f i A f B i dom f f i f B A
9 5 4 bnj1083 f B n χ
10 2 bnj1095 ψ i ψ
11 10 5 bnj1096 χ i χ
12 3 bnj1098 j i i n n D j n i = suc j
13 5 bnj1232 χ n D
14 13 3anim3i i i n χ i i n n D
15 12 14 bnj1101 j i i n χ j n i = suc j
16 ancl i i n χ j n i = suc j i i n χ i i n χ j n i = suc j
17 15 16 bnj101 j i i n χ i i n χ j n i = suc j
18 6 imbi2i i i n χ θ i i n χ i i n χ j n i = suc j
19 18 exbii j i i n χ θ j i i n χ i i n χ j n i = suc j
20 17 19 mpbir j i i n χ θ
21 bnj213 pred y A R A
22 21 bnj226 y f j pred y A R A
23 simpr j n i = suc j i = suc j
24 6 23 simplbiim θ i = suc j
25 simp2 i i n χ i n
26 13 3ad2ant3 i i n χ n D
27 3 bnj923 n D n ω
28 elnn i n n ω i ω
29 27 28 sylan2 i n n D i ω
30 25 26 29 syl2anc i i n χ i ω
31 6 30 bnj832 θ i ω
32 vex j V
33 32 bnj216 i = suc j j i
34 elnn j i i ω j ω
35 33 34 sylan i = suc j i ω j ω
36 24 31 35 syl2anc θ j ω
37 6 25 bnj832 θ i n
38 24 37 eqeltrrd θ suc j n
39 2 bnj589 ψ j ω suc j n f suc j = y f j pred y A R
40 39 biimpi ψ j ω suc j n f suc j = y f j pred y A R
41 40 bnj708 n D f Fn n φ ψ j ω suc j n f suc j = y f j pred y A R
42 rsp j ω suc j n f suc j = y f j pred y A R j ω suc j n f suc j = y f j pred y A R
43 41 42 syl n D f Fn n φ ψ j ω suc j n f suc j = y f j pred y A R
44 5 43 sylbi χ j ω suc j n f suc j = y f j pred y A R
45 44 3ad2ant3 i i n χ j ω suc j n f suc j = y f j pred y A R
46 6 45 bnj832 θ j ω suc j n f suc j = y f j pred y A R
47 36 38 46 mp2d θ f suc j = y f j pred y A R
48 fveqeq2 i = suc j f i = y f j pred y A R f suc j = y f j pred y A R
49 24 48 syl θ f i = y f j pred y A R f suc j = y f j pred y A R
50 47 49 mpbird θ f i = y f j pred y A R
51 22 50 bnj1262 θ f i A
52 20 51 bnj1023 j i i n χ f i A
53 3anass i i n χ i i n χ
54 53 imbi1i i i n χ f i A i i n χ f i A
55 54 exbii j i i n χ f i A j i i n χ f i A
56 52 55 mpbi j i i n χ f i A
57 1 biimpi φ f = pred X A R
58 5 57 bnj771 χ f = pred X A R
59 fveq2 i = f i = f
60 bnj213 pred X A R A
61 sseq1 f = pred X A R f A pred X A R A
62 60 61 mpbiri f = pred X A R f A
63 sseq1 f i = f f i A f A
64 63 biimpar f i = f f A f i A
65 59 62 64 syl2an i = f = pred X A R f i A
66 58 65 sylan2 i = χ f i A
67 66 adantrl i = i n χ f i A
68 56 67 bnj1109 j i n χ f i A
69 19.9v j i n χ f i A i n χ f i A
70 68 69 mpbi i n χ f i A
71 70 expcom χ i n f i A
72 fndm f Fn n dom f = n
73 5 72 bnj770 χ dom f = n
74 eleq2 dom f = n i dom f i n
75 74 imbi1d dom f = n i dom f f i A i n f i A
76 73 75 syl χ i dom f f i A i n f i A
77 71 76 mpbird χ i dom f f i A
78 11 77 hbralrimi χ i dom f f i A
79 78 exlimiv n χ i dom f f i A
80 9 79 sylbi f B i dom f f i A
81 ss2iun i dom f f i A i dom f f i i dom f A
82 bnj1143 i dom f A A
83 81 82 sstrdi i dom f f i A i dom f f i A
84 80 83 syl f B i dom f f i A
85 8 84 mprg f B i dom f f i f B A
86 4 bnj1317 w B f w B
87 86 bnj1146 f B A A
88 85 87 sstri f B i dom f f i A
89 7 88 eqsstri trCl X A R A