Metamath Proof Explorer

Theorem bnj594

Description: Technical lemma for bnj852 . 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 bnj594.1 
|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj594.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj594.3 
|- ( ch <-> ( f Fn n /\ ph /\ ps ) )
bnj594.7 
|- D = ( _om \ { (/) } )
bnj594.9 
|- ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) )
bnj594.10 
|- ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) )
bnj594.11 
|- ( ch' <-> ( g Fn n /\ ph' /\ ps' ) )
bnj594.15 
|- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
bnj594.16 
|- ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) )
bnj594.17 
|- ( ta <-> A. k e. n ( k _E j -> [. k / j ]. th ) )
Assertion bnj594 
|- ( ( j e. n /\ ta ) -> th )

Proof

Step Hyp Ref Expression
1 bnj594.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
2 bnj594.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj594.3 
 |-  ( ch <-> ( f Fn n /\ ph /\ ps ) )
4 bnj594.7 
 |-  D = ( _om \ { (/) } )
5 bnj594.9 
 |-  ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) )
6 bnj594.10 
 |-  ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) )
7 bnj594.11 
 |-  ( ch' <-> ( g Fn n /\ ph' /\ ps' ) )
8 bnj594.15 
 |-  ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
9 bnj594.16 
 |-  ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) )
10 bnj594.17 
 |-  ( ta <-> A. k e. n ( k _E j -> [. k / j ]. th ) )
11 3 simp2bi 
 |-  ( ch -> ph )
12 11 1 sylib 
 |-  ( ch -> ( f ` (/) ) = _pred ( x , A , R ) )
13 7 simp2bi 
 |-  ( ch' -> ph' )
14 13 5 sylib 
 |-  ( ch' -> ( g ` (/) ) = _pred ( x , A , R ) )
15 eqtr3 
 |-  ( ( ( f ` (/) ) = _pred ( x , A , R ) /\ ( g ` (/) ) = _pred ( x , A , R ) ) -> ( f ` (/) ) = ( g ` (/) ) )
16 12 14 15 syl2an 
 |-  ( ( ch /\ ch' ) -> ( f ` (/) ) = ( g ` (/) ) )
17 16 3adant1 
 |-  ( ( n e. D /\ ch /\ ch' ) -> ( f ` (/) ) = ( g ` (/) ) )
18 fveq2 
 |-  ( j = (/) -> ( f ` j ) = ( f ` (/) ) )
19 fveq2 
 |-  ( j = (/) -> ( g ` j ) = ( g ` (/) ) )
20 18 19 eqeq12d 
 |-  ( j = (/) -> ( ( f ` j ) = ( g ` j ) <-> ( f ` (/) ) = ( g ` (/) ) ) )
21 17 20 imbitrrid 
 |-  ( j = (/) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
22 21 8 sylibr 
 |-  ( j = (/) -> th )
23 22 a1d 
 |-  ( j = (/) -> ( ( j e. n /\ ta ) -> th ) )
24 bnj253 
 |-  ( ( n e. D /\ n e. D /\ ch /\ ch' ) <-> ( ( n e. D /\ n e. D ) /\ ch /\ ch' ) )
25 bnj252 
 |-  ( ( n e. D /\ n e. D /\ ch /\ ch' ) <-> ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) )
26 anidm 
 |-  ( ( n e. D /\ n e. D ) <-> n e. D )
27 26 3anbi1i 
 |-  ( ( ( n e. D /\ n e. D ) /\ ch /\ ch' ) <-> ( n e. D /\ ch /\ ch' ) )
28 24 25 27 3bitr3i 
 |-  ( ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) <-> ( n e. D /\ ch /\ ch' ) )
29 df-bnj17 
 |-  ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) <-> ( ( j =/= (/) /\ j e. n /\ n e. D ) /\ ta ) )
30 10 bnj1095 
 |-  ( ta -> A. k ta )
31 30 bnj1352 
 |-  ( ( ( j =/= (/) /\ j e. n /\ n e. D ) /\ ta ) -> A. k ( ( j =/= (/) /\ j e. n /\ n e. D ) /\ ta ) )
32 29 31 hbxfrbi 
 |-  ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) -> A. k ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) )
33 bnj170 
 |-  ( ( j =/= (/) /\ j e. n /\ n e. D ) <-> ( ( j e. n /\ n e. D ) /\ j =/= (/) ) )
34 4 bnj923 
 |-  ( n e. D -> n e. _om )
35 elnn 
 |-  ( ( j e. n /\ n e. _om ) -> j e. _om )
36 34 35 sylan2 
 |-  ( ( j e. n /\ n e. D ) -> j e. _om )
37 36 anim1i 
 |-  ( ( ( j e. n /\ n e. D ) /\ j =/= (/) ) -> ( j e. _om /\ j =/= (/) ) )
38 33 37 sylbi 
 |-  ( ( j =/= (/) /\ j e. n /\ n e. D ) -> ( j e. _om /\ j =/= (/) ) )
39 nnsuc 
 |-  ( ( j e. _om /\ j =/= (/) ) -> E. k e. _om j = suc k )
40 rexex 
 |-  ( E. k e. _om j = suc k -> E. k j = suc k )
41 38 39 40 3syl 
 |-  ( ( j =/= (/) /\ j e. n /\ n e. D ) -> E. k j = suc k )
42 41 bnj721 
 |-  ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) -> E. k j = suc k )
43 32 42 bnj596 
 |-  ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) -> E. k ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) /\ j = suc k ) )
44 bnj667 
 |-  ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) -> ( j e. n /\ n e. D /\ ta ) )
45 44 anim1i 
 |-  ( ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) /\ j = suc k ) -> ( ( j e. n /\ n e. D /\ ta ) /\ j = suc k ) )
46 bnj258 
 |-  ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) <-> ( ( j e. n /\ n e. D /\ ta ) /\ j = suc k ) )
47 45 46 sylibr 
 |-  ( ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) /\ j = suc k ) -> ( j e. n /\ n e. D /\ j = suc k /\ ta ) )
48 df-bnj17 
 |-  ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) <-> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ta ) )
49 bnj219 
 |-  ( j = suc k -> k _E j )
50 49 3ad2ant3 
 |-  ( ( j e. n /\ n e. D /\ j = suc k ) -> k _E j )
51 50 adantr 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ta ) -> k _E j )
52 vex 
 |-  k e. _V
53 52 bnj216 
 |-  ( j = suc k -> k e. j )
54 df-3an 
 |-  ( ( k e. j /\ j e. n /\ n e. D ) <-> ( ( k e. j /\ j e. n ) /\ n e. D ) )
55 3anrot 
 |-  ( ( k e. j /\ j e. n /\ n e. D ) <-> ( j e. n /\ n e. D /\ k e. j ) )
56 ancom 
 |-  ( ( ( k e. j /\ j e. n ) /\ n e. D ) <-> ( n e. D /\ ( k e. j /\ j e. n ) ) )
57 54 55 56 3bitr3i 
 |-  ( ( j e. n /\ n e. D /\ k e. j ) <-> ( n e. D /\ ( k e. j /\ j e. n ) ) )
58 eldifi 
 |-  ( n e. ( _om \ { (/) } ) -> n e. _om )
59 58 4 eleq2s 
 |-  ( n e. D -> n e. _om )
60 nnord 
 |-  ( n e. _om -> Ord n )
61 ordtr1 
 |-  ( Ord n -> ( ( k e. j /\ j e. n ) -> k e. n ) )
62 59 60 61 3syl 
 |-  ( n e. D -> ( ( k e. j /\ j e. n ) -> k e. n ) )
63 62 imp 
 |-  ( ( n e. D /\ ( k e. j /\ j e. n ) ) -> k e. n )
64 57 63 sylbi 
 |-  ( ( j e. n /\ n e. D /\ k e. j ) -> k e. n )
65 53 64 syl3an3 
 |-  ( ( j e. n /\ n e. D /\ j = suc k ) -> k e. n )
66 rsp 
 |-  ( A. k e. n ( k _E j -> [. k / j ]. th ) -> ( k e. n -> ( k _E j -> [. k / j ]. th ) ) )
67 10 66 sylbi 
 |-  ( ta -> ( k e. n -> ( k _E j -> [. k / j ]. th ) ) )
68 65 67 mpan9 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ta ) -> ( k _E j -> [. k / j ]. th ) )
69 51 68 mpd 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ta ) -> [. k / j ]. th )
70 48 69 sylbi 
 |-  ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) -> [. k / j ]. th )
71 70 anim1i 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( [. k / j ]. th /\ ( n e. D /\ ch /\ ch' ) ) )
72 bnj252 
 |-  ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) <-> ( [. k / j ]. th /\ ( n e. D /\ ch /\ ch' ) ) )
73 71 72 sylibr 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) )
74 bnj446 
 |-  ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) <-> ( ( n e. D /\ ch /\ ch' ) /\ [. k / j ]. th ) )
75 pm3.35 
 |-  ( ( ( n e. D /\ ch /\ ch' ) /\ ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) -> ( f ` k ) = ( g ` k ) )
76 9 75 sylan2b 
 |-  ( ( ( n e. D /\ ch /\ ch' ) /\ [. k / j ]. th ) -> ( f ` k ) = ( g ` k ) )
77 74 76 sylbi 
 |-  ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) )
78 iuneq1 
 |-  ( ( f ` k ) = ( g ` k ) -> U_ y e. ( f ` k ) _pred ( y , A , R ) = U_ y e. ( g ` k ) _pred ( y , A , R ) )
79 73 77 78 3syl 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> U_ y e. ( f ` k ) _pred ( y , A , R ) = U_ y e. ( g ` k ) _pred ( y , A , R ) )
80 bnj658 
 |-  ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) -> ( j e. n /\ n e. D /\ j = suc k ) )
81 3 simp3bi 
 |-  ( ch -> ps )
82 7 simp3bi 
 |-  ( ch' -> ps' )
83 81 82 bnj240 
 |-  ( ( n e. D /\ ch /\ ch' ) -> ( ps /\ ps' ) )
84 80 83 anim12i 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) )
85 simpl 
 |-  ( ( ps /\ ps' ) -> ps )
86 85 anim2i 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps ) )
87 simp3 
 |-  ( ( j e. n /\ n e. D /\ j = suc k ) -> j = suc k )
88 87 anim1i 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps ) -> ( j = suc k /\ ps ) )
89 simpl1 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps ) ) -> j e. n )
90 df-3an 
 |-  ( ( j e. n /\ n e. D /\ j = suc k ) <-> ( ( j e. n /\ n e. D ) /\ j = suc k ) )
91 90 biancomi 
 |-  ( ( j e. n /\ n e. D /\ j = suc k ) <-> ( j = suc k /\ ( j e. n /\ n e. D ) ) )
92 elnn 
 |-  ( ( k e. j /\ j e. _om ) -> k e. _om )
93 53 36 92 syl2an 
 |-  ( ( j = suc k /\ ( j e. n /\ n e. D ) ) -> k e. _om )
94 91 93 sylbi 
 |-  ( ( j e. n /\ n e. D /\ j = suc k ) -> k e. _om )
95 2 bnj589 
 |-  ( ps <-> A. k e. _om ( suc k e. n -> ( f ` suc k ) = U_ y e. ( f ` k ) _pred ( y , A , R ) ) )
96 95 bnj590 
 |-  ( ( j = suc k /\ ps ) -> ( k e. _om -> ( j e. n -> ( f ` j ) = U_ y e. ( f ` k ) _pred ( y , A , R ) ) ) )
97 94 96 mpan9 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps ) ) -> ( j e. n -> ( f ` j ) = U_ y e. ( f ` k ) _pred ( y , A , R ) ) )
98 89 97 mpd 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps ) ) -> ( f ` j ) = U_ y e. ( f ` k ) _pred ( y , A , R ) )
99 88 98 syldan 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps ) -> ( f ` j ) = U_ y e. ( f ` k ) _pred ( y , A , R ) )
100 84 86 99 3syl 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = U_ y e. ( f ` k ) _pred ( y , A , R ) )
101 simpr 
 |-  ( ( ps /\ ps' ) -> ps' )
102 101 anim2i 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) )
103 87 anim1i 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) -> ( j = suc k /\ ps' ) )
104 simpl1 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> j e. n )
105 6 bnj589 
 |-  ( ps' <-> A. k e. _om ( suc k e. n -> ( g ` suc k ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) )
106 105 bnj590 
 |-  ( ( j = suc k /\ ps' ) -> ( k e. _om -> ( j e. n -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) )
107 94 106 mpan9 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> ( j e. n -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) )
108 104 107 mpd 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) )
109 103 108 syldan 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) )
110 84 102 109 3syl 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) )
111 79 100 110 3eqtr4d 
 |-  ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) )
112 111 ex 
 |-  ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
113 47 112 syl 
 |-  ( ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) /\ j = suc k ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
114 43 113 bnj593 
 |-  ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) -> E. k ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
115 bnj258 
 |-  ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) <-> ( ( j =/= (/) /\ j e. n /\ ta ) /\ n e. D ) )
116 19.9v 
 |-  ( E. k ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
117 114 115 116 3imtr3i 
 |-  ( ( ( j =/= (/) /\ j e. n /\ ta ) /\ n e. D ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
118 117 expimpd 
 |-  ( ( j =/= (/) /\ j e. n /\ ta ) -> ( ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) )
119 28 118 biimtrrid 
 |-  ( ( j =/= (/) /\ j e. n /\ ta ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
120 119 8 sylibr 
 |-  ( ( j =/= (/) /\ j e. n /\ ta ) -> th )
121 120 3expib 
 |-  ( j =/= (/) -> ( ( j e. n /\ ta ) -> th ) )
122 23 121 pm2.61ine 
 |-  ( ( j e. n /\ ta ) -> th )